1. Cryptids
  2. Semantics
  3. Zf
  4. Soundness
Imports
/- Copyright (c) 2026 Google LLC. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ module public import Cryptids.Propositions public import Mathlib.Tactic.Ring

Gödel Numbering, Hilbert System, and Soundness of zf2.nql in Mathlib's ZFSet

This module formalizes the logical core of Stefan O'Rear's zf2.nql ZF proof enumerator:

    Cantor Unpairing: the inverse cantorUnpair of cantorPair (Cryptids.Propositions), with bijection theorems cantorUnpair_cantorPair and cantorPair_cantorUnpair.

    Total Tarski Truth Predicate zfHolds: a well-founded satisfaction relation on all natural numbers n : ℕ under valuations v : ℕ → ZFSet.{u}, with [simp] Tarski equations for every constructor and agreement with the structural ZFFormula.Holds.

    Soundness: zfProvable_zfHolds, zfProvable_sound_zfSet, and not_zfInconsistent : ¬ ZFInconsistent, derived from Mathlib's ZFSet.{0} model (ZFSet.ext, ZFSet.powerset, ZFSet.sUnion, ZFSet.sep/ZFSet.image for Replacement, and an explicit singleton-closed witness for Infinity).

@[expose] public sectionnamespace ConjectureMachines.Semantics.Zf

Section 1: Basic [simp] Lemmas for Formula Encodings

@[simp] theorem cantorPair_zero_zero : cantorPair 0 0 = 0 := rfl@[simp] theorem cantorPair_zero_one : cantorPair 0 1 = 1 := rfl@[simp] theorem zfEq_zero_zero : zfEq 0 0 = 0 := rfl@[simp] theorem zfMem_zero_zero : zfMem 0 0 = 1 := rfl

Section 1b: Cantor Unpairing and Bounds

One step along the Cantor diagonal enumeration of ℕ × ℕ.

def cantorStep (p : ℕ × ℕ) : ℕ × ℕ := match p.2 with | 0 => (0, p.1 + 1) | y + 1 => (p.1 + 1, y)

Inverse of cantorPair, defined by iterating cantorStep from (0, 0).

def cantorUnpair : ℕ → ℕ × ℕ | 0 => (0, 0) | z + 1 => cantorStep (cantorUnpair z)@[simp] theorem cantorUnpair_zero : cantorUnpair 0 = (0, 0) := rfl@[simp] theorem cantorUnpair_succ (z : ℕ) : cantorUnpair (z + 1) = cantorStep (cantorUnpair z) := rfltheorem tri_succ (n : ℕ) : (n + 1) * (n + 1 + 1) / 2 = n * (n + 1) / 2 + (n + 1) := n:ℕ⊢ (n + 1) * (n + 1 + 1) / 2 = n * (n + 1) / 2 + (n + 1) n:ℕh:(n + 1) * (n + 1 + 1) = n * (n + 1) + (n + 1) * 2⊢ (n + 1) * (n + 1 + 1) / 2 = n * (n + 1) / 2 + (n + 1) All goals completed! 🐙private theorem le_tri (n : ℕ) : n ≤ n * (n + 1) / 2 := n:ℕ⊢ n ≤ n * (n + 1) / 2 cases n with ⊢ 0 ≤ 0 * (0 + 1) / 2 All goals completed! 🐙 m:ℕ⊢ m + 1 ≤ (m + 1) * (m + 1 + 1) / 2 m:ℕthis:(m + 1) * (m + 1 + 1) / 2 = m * (m + 1) / 2 + (m + 1)⊢ m + 1 ≤ (m + 1) * (m + 1 + 1) / 2 All goals completed! 🐙theorem add_le_cantorPair (x y : ℕ) : x + y ≤ cantorPair x y := x:ℕy:ℕ⊢ x + y ≤ cantorPair x y x:ℕy:ℕ⊢ x + y ≤ x + (x + y) * (x + y + 1) / 2 x:ℕy:ℕthis:x + y ≤ (x + y) * (x + y + 1) / 2⊢ x + y ≤ x + (x + y) * (x + y + 1) / 2 All goals completed! 🐙theorem le_cantorPair_left (x y : ℕ) : x ≤ cantorPair x y := x:ℕy:ℕ⊢ x ≤ cantorPair x y x:ℕy:ℕthis:x + y ≤ cantorPair x y⊢ x ≤ cantorPair x y All goals completed! 🐙theorem le_cantorPair_right (x y : ℕ) : y ≤ cantorPair x y := x:ℕy:ℕ⊢ y ≤ cantorPair x y x:ℕy:ℕthis:x + y ≤ cantorPair x y⊢ y ≤ cantorPair x y All goals completed! 🐙theorem lt_cantorPair_left_of_pos (x y : ℕ) (hy : 0 < y) : x < cantorPair x y := x:ℕy:ℕhy:0 < y⊢ x < cantorPair x y x:ℕy:ℕhy:0 < ythis:x + y ≤ cantorPair x y⊢ x < cantorPair x y All goals completed! 🐙theorem cantorPair_zero_succ (x : ℕ) : cantorPair 0 (x + 1) = cantorPair x 0 + 1 := x:ℕ⊢ cantorPair 0 (x + 1) = cantorPair x 0 + 1 x:ℕ⊢ 0 + (0 + (x + 1)) * (0 + (x + 1) + 1) / 2 = x + (x + 0) * (x + 0 + 1) / 2 + 1 x:ℕ⊢ (x + 1) * (x + 1 + 1) / 2 = x + x * (x + 1) / 2 + 1 x:ℕthis:(x + 1) * (x + 1 + 1) / 2 = x * (x + 1) / 2 + (x + 1)⊢ (x + 1) * (x + 1 + 1) / 2 = x + x * (x + 1) / 2 + 1 All goals completed! 🐙theorem cantorPair_succ_left (x y : ℕ) : cantorPair (x + 1) y = cantorPair x (y + 1) + 1 := x:ℕy:ℕ⊢ cantorPair (x + 1) y = cantorPair x (y + 1) + 1 x:ℕy:ℕ⊢ x + 1 + (x + 1 + y) * (x + 1 + y + 1) / 2 = x + (x + (y + 1)) * (x + (y + 1) + 1) / 2 + 1 x:ℕy:ℕh1:x + 1 + y = x + (y + 1)⊢ x + 1 + (x + 1 + y) * (x + 1 + y + 1) / 2 = x + (x + (y + 1)) * (x + (y + 1) + 1) / 2 + 1 x:ℕy:ℕh1:x + 1 + y = x + (y + 1)⊢ x + 1 + (x + (y + 1)) * (x + (y + 1) + 1) / 2 = x + (x + (y + 1)) * (x + (y + 1) + 1) / 2 + 1 All goals completed! 🐙theorem cantorPair_cantorStep (p : ℕ × ℕ) : cantorPair (cantorStep p).1 (cantorStep p).2 = cantorPair p.1 p.2 + 1 := p:ℕ × ℕ⊢ cantorPair (cantorStep p).1 (cantorStep p).2 = cantorPair p.1 p.2 + 1 x:ℕ⊢ cantorPair (cantorStep (x, 0)).1 (cantorStep (x, 0)).2 = cantorPair (x, 0).1 (x, 0).2 + 1x:ℕy:ℕ⊢ cantorPair (cantorStep (x, y + 1)).1 (cantorStep (x, y + 1)).2 = cantorPair (x, y + 1).1 (x, y + 1).2 + 1 x:ℕ⊢ cantorPair (cantorStep (x, 0)).1 (cantorStep (x, 0)).2 = cantorPair (x, 0).1 (x, 0).2 + 1 All goals completed! 🐙 x:ℕy:ℕ⊢ cantorPair (cantorStep (x, y + 1)).1 (cantorStep (x, y + 1)).2 = cantorPair (x, y + 1).1 (x, y + 1).2 + 1 All goals completed! 🐙@[simp] theorem cantorPair_cantorUnpair (z : ℕ) : cantorPair (cantorUnpair z).1 (cantorUnpair z).2 = z := z:ℕ⊢ cantorPair (cantorUnpair z).1 (cantorUnpair z).2 = z induction z with ⊢ cantorPair (cantorUnpair 0).1 (cantorUnpair 0).2 = 0 All goals completed! 🐙 z:ℕih:cantorPair (cantorUnpair z).1 (cantorUnpair z).2 = z⊢ cantorPair (cantorUnpair (z + 1)).1 (cantorUnpair (z + 1)).2 = z + 1 z:ℕih:cantorPair (cantorUnpair z).1 (cantorUnpair z).2 = z⊢ cantorPair (cantorStep (cantorUnpair z)).1 (cantorStep (cantorUnpair z)).2 = z + 1 All goals completed! 🐙private theorem cantorUnpair_cantorPair_aux (s : ℕ) : ∀ x y, x + y = s → cantorUnpair (cantorPair x y) = (x, y) := s:ℕ⊢ ∀ (x y : ℕ), x + y = s → cantorUnpair (cantorPair x y) = (x, y) induction s with ⊢ ∀ (x y : ℕ), x + y = 0 → cantorUnpair (cantorPair x y) = (x, y) x:ℕy:ℕh:x + y = 0⊢ cantorUnpair (cantorPair x y) = (x, y) h:0 + 0 = 0⊢ cantorUnpair (cantorPair 0 0) = (0, 0) All goals completed! 🐙 s:ℕihs:∀ (x y : ℕ), x + y = s → cantorUnpair (cantorPair x y) = (x, y)⊢ ∀ (x y : ℕ), x + y = s + 1 → cantorUnpair (cantorPair x y) = (x, y) s:ℕihs:∀ (x y : ℕ), x + y = s → cantorUnpair (cantorPair x y) = (x, y)x:ℕ⊢ ∀ (y : ℕ), x + y = s + 1 → cantorUnpair (cantorPair x y) = (x, y) induction x with s:ℕihs:∀ (x y : ℕ), x + y = s → cantorUnpair (cantorPair x y) = (x, y)⊢ ∀ (y : ℕ), 0 + y = s + 1 → cantorUnpair (cantorPair 0 y) = (0, y) s:ℕihs:∀ (x y : ℕ), x + y = s → cantorUnpair (cantorPair x y) = (x, y)y:ℕhy:0 + y = s + 1⊢ cantorUnpair (cantorPair 0 y) = (0, y) s:ℕihs:∀ (x y : ℕ), x + y = s → cantorUnpair (cantorPair x y) = (x, y)hy:0 + (s + 1) = s + 1⊢ cantorUnpair (cantorPair 0 (s + 1)) = (0, s + 1) s:ℕihs:∀ (x y : ℕ), x + y = s → cantorUnpair (cantorPair x y) = (x, y)hy:0 + (s + 1) = s + 1⊢ cantorStep (s, 0) = (0, s + 1) All goals completed! 🐙 s:ℕihs:∀ (x y : ℕ), x + y = s → cantorUnpair (cantorPair x y) = (x, y)x:ℕihx:∀ (y : ℕ), x + y = s + 1 → cantorUnpair (cantorPair x y) = (x, y)⊢ ∀ (y : ℕ), x + 1 + y = s + 1 → cantorUnpair (cantorPair (x + 1) y) = (x + 1, y) s:ℕihs:∀ (x y : ℕ), x + y = s → cantorUnpair (cantorPair x y) = (x, y)x:ℕihx:∀ (y : ℕ), x + y = s + 1 → cantorUnpair (cantorPair x y) = (x, y)y:ℕhy:x + 1 + y = s + 1⊢ cantorUnpair (cantorPair (x + 1) y) = (x + 1, y) s:ℕihs:∀ (x y : ℕ), x + y = s → cantorUnpair (cantorPair x y) = (x, y)x:ℕihx:∀ (y : ℕ), x + y = s + 1 → cantorUnpair (cantorPair x y) = (x, y)y:ℕhy:x + 1 + y = s + 1⊢ cantorStep (x, y + 1) = (x + 1, y) All goals completed! 🐙@[simp] theorem cantorUnpair_cantorPair (x y : ℕ) : cantorUnpair (cantorPair x y) = (x, y) := cantorUnpair_cantorPair_aux (x + y) x y rfltheorem cantorUnpair_fst_lt_of_snd_pos {n : ℕ} (h : 0 < (cantorUnpair n).2) : (cantorUnpair n).1 < n := n:ℕh:0 < (cantorUnpair n).2⊢ (cantorUnpair n).1 < n n:ℕh:0 < (cantorUnpair n).2h1:(cantorUnpair n).1 < cantorPair (cantorUnpair n).1 (cantorUnpair n).2⊢ (cantorUnpair n).1 < n All goals completed! 🐙theorem cantorUnpair_fst_le (m : ℕ) : (cantorUnpair m).1 ≤ m := m:ℕ⊢ (cantorUnpair m).1 ≤ m m:ℕh1:(cantorUnpair m).1 ≤ cantorPair (cantorUnpair m).1 (cantorUnpair m).2⊢ (cantorUnpair m).1 ≤ m All goals completed! 🐙theorem cantorUnpair_snd_le (m : ℕ) : (cantorUnpair m).2 ≤ m := m:ℕ⊢ (cantorUnpair m).2 ≤ m m:ℕh1:(cantorUnpair m).2 ≤ cantorPair (cantorUnpair m).1 (cantorUnpair m).2⊢ (cantorUnpair m).2 ≤ m All goals completed! 🐙

Section 1c: Total Tarski Truth Predicate on ℕ

Total Tarski satisfaction predicate on Gödel numbers n : ℕ under valuation v : ℕ → ZFSet.{u}.

def zfHolds (n : ℕ) (v : ℕ → ZFSet.{u}) : Prop := let m := (cantorUnpair n).1 let op := (cantorUnpair n).2 if h0 : op = 0 then v (cantorUnpair m).1 = v (cantorUnpair m).2 else if h1 : op = 1 then v (cantorUnpair m).1 ∈ v (cantorUnpair m).2 else if h2 : op = 2 then have hm : m < n := cantorUnpair_fst_lt_of_snd_pos (n:ℕv:ℕ → ZFSet.{u}m:ℕ := (cantorUnpair n).1op:ℕ := (cantorUnpair n).2h0:¬op = 0h1:¬op = 1h2:op = 2⊢ 0 < (cantorUnpair n).2 All goals completed! 🐙) have hp : (cantorUnpair m).1 < n := Nat.lt_of_le_of_lt (cantorUnpair_fst_le m) hm have hq : (cantorUnpair m).2 < n := Nat.lt_of_le_of_lt (cantorUnpair_snd_le m) hm zfHolds (cantorUnpair m).1 v → zfHolds (cantorUnpair m).2 v else if h3 : op = 3 then have hm : m < n := cantorUnpair_fst_lt_of_snd_pos (n:ℕv:ℕ → ZFSet.{u}m:ℕ := (cantorUnpair n).1op:ℕ := (cantorUnpair n).2h0:¬op = 0h1:¬op = 1h2:¬op = 2h3:op = 3⊢ 0 < (cantorUnpair n).2 All goals completed! 🐙) ¬ zfHolds m v else if h4 : op = 4 then have hm : m < n := cantorUnpair_fst_lt_of_snd_pos (n:ℕv:ℕ → ZFSet.{u}m:ℕ := (cantorUnpair n).1op:ℕ := (cantorUnpair n).2h0:¬op = 0h1:¬op = 1h2:¬op = 2h3:¬op = 3h4:op = 4⊢ 0 < (cantorUnpair n).2 All goals completed! 🐙) have hp : (cantorUnpair m).2 < n := Nat.lt_of_le_of_lt (cantorUnpair_snd_le m) hm ∀ s : ZFSet.{u}, zfHolds (cantorUnpair m).2 (Function.update v (cantorUnpair m).1 s) else True termination_by n@[simp] theorem zfHolds_zfEq (x y : ℕ) (v : ℕ → ZFSet.{u}) : zfHolds (zfEq x y) v ↔ v x = v y := x:ℕy:ℕv:ℕ → ZFSet.{u}⊢ zfHolds (zfEq x y) v ↔ v x = v y x:ℕy:ℕv:ℕ → ZFSet.{u}⊢ (if h0 : (cantorUnpair (zfEq x y)).2 = 0 then v (cantorUnpair (cantorUnpair (zfEq x y)).1).1 = v (cantorUnpair (cantorUnpair (zfEq x y)).1).2 else if h1 : (cantorUnpair (zfEq x y)).2 = 1 then v (cantorUnpair (cantorUnpair (zfEq x y)).1).1 ∈ v (cantorUnpair (cantorUnpair (zfEq x y)).1).2 else if h2 : (cantorUnpair (zfEq x y)).2 = 2 then have hm := ⋯; have hp := ⋯; have hq := ⋯; zfHolds (cantorUnpair (cantorUnpair (zfEq x y)).1).1 v → zfHolds (cantorUnpair (cantorUnpair (zfEq x y)).1).2 v else if h3 : (cantorUnpair (zfEq x y)).2 = 3 then have hm := ⋯; ¬zfHolds (cantorUnpair (zfEq x y)).1 v else if h4 : (cantorUnpair (zfEq x y)).2 = 4 then have hm := ⋯; have hp := ⋯; ∀ (s : ZFSet.{u}), zfHolds (cantorUnpair (cantorUnpair (zfEq x y)).1).2 (Function.update v (cantorUnpair (cantorUnpair (zfEq x y)).1).1 s) else True) ↔ v x = v y All goals completed! 🐙@[simp] theorem zfHolds_zfMem (x y : ℕ) (v : ℕ → ZFSet.{u}) : zfHolds (zfMem x y) v ↔ v x ∈ v y := x:ℕy:ℕv:ℕ → ZFSet.{u}⊢ zfHolds (zfMem x y) v ↔ v x ∈ v y x:ℕy:ℕv:ℕ → ZFSet.{u}⊢ (if h0 : (cantorUnpair (zfMem x y)).2 = 0 then v (cantorUnpair (cantorUnpair (zfMem x y)).1).1 = v (cantorUnpair (cantorUnpair (zfMem x y)).1).2 else if h1 : (cantorUnpair (zfMem x y)).2 = 1 then v (cantorUnpair (cantorUnpair (zfMem x y)).1).1 ∈ v (cantorUnpair (cantorUnpair (zfMem x y)).1).2 else if h2 : (cantorUnpair (zfMem x y)).2 = 2 then have hm := ⋯; have hp := ⋯; have hq := ⋯; zfHolds (cantorUnpair (cantorUnpair (zfMem x y)).1).1 v → zfHolds (cantorUnpair (cantorUnpair (zfMem x y)).1).2 v else if h3 : (cantorUnpair (zfMem x y)).2 = 3 then have hm := ⋯; ¬zfHolds (cantorUnpair (zfMem x y)).1 v else if h4 : (cantorUnpair (zfMem x y)).2 = 4 then have hm := ⋯; have hp := ⋯; ∀ (s : ZFSet.{u}), zfHolds (cantorUnpair (cantorUnpair (zfMem x y)).1).2 (Function.update v (cantorUnpair (cantorUnpair (zfMem x y)).1).1 s) else True) ↔ v x ∈ v y All goals completed! 🐙@[simp] theorem zfHolds_zfImp (φ ψ : ℕ) (v : ℕ → ZFSet.{u}) : zfHolds (zfImp φ ψ) v ↔ (zfHolds φ v → zfHolds ψ v) := φ:ℕψ:ℕv:ℕ → ZFSet.{u}⊢ zfHolds (zfImp φ ψ) v ↔ zfHolds φ v → zfHolds ψ v φ:ℕψ:ℕv:ℕ → ZFSet.{u}⊢ (if h0 : (cantorUnpair (zfImp φ ψ)).2 = 0 then v (cantorUnpair (cantorUnpair (zfImp φ ψ)).1).1 = v (cantorUnpair (cantorUnpair (zfImp φ ψ)).1).2 else if h1 : (cantorUnpair (zfImp φ ψ)).2 = 1 then v (cantorUnpair (cantorUnpair (zfImp φ ψ)).1).1 ∈ v (cantorUnpair (cantorUnpair (zfImp φ ψ)).1).2 else if h2 : (cantorUnpair (zfImp φ ψ)).2 = 2 then have hm := ⋯; have hp := ⋯; have hq := ⋯; zfHolds (cantorUnpair (cantorUnpair (zfImp φ ψ)).1).1 v → zfHolds (cantorUnpair (cantorUnpair (zfImp φ ψ)).1).2 v else if h3 : (cantorUnpair (zfImp φ ψ)).2 = 3 then have hm := ⋯; ¬zfHolds (cantorUnpair (zfImp φ ψ)).1 v else if h4 : (cantorUnpair (zfImp φ ψ)).2 = 4 then have hm := ⋯; have hp := ⋯; ∀ (s : ZFSet.{u}), zfHolds (cantorUnpair (cantorUnpair (zfImp φ ψ)).1).2 (Function.update v (cantorUnpair (cantorUnpair (zfImp φ ψ)).1).1 s) else True) ↔ zfHolds φ v → zfHolds ψ v All goals completed! 🐙@[simp] theorem zfHolds_zfNot (φ : ℕ) (v : ℕ → ZFSet.{u}) : zfHolds (zfNot φ) v ↔ ¬ zfHolds φ v := φ:ℕv:ℕ → ZFSet.{u}⊢ zfHolds (zfNot φ) v ↔ ¬zfHolds φ v φ:ℕv:ℕ → ZFSet.{u}⊢ (if h0 : (cantorUnpair (zfNot φ)).2 = 0 then v (cantorUnpair (cantorUnpair (zfNot φ)).1).1 = v (cantorUnpair (cantorUnpair (zfNot φ)).1).2 else if h1 : (cantorUnpair (zfNot φ)).2 = 1 then v (cantorUnpair (cantorUnpair (zfNot φ)).1).1 ∈ v (cantorUnpair (cantorUnpair (zfNot φ)).1).2 else if h2 : (cantorUnpair (zfNot φ)).2 = 2 then have hm := ⋯; have hp := ⋯; have hq := ⋯; zfHolds (cantorUnpair (cantorUnpair (zfNot φ)).1).1 v → zfHolds (cantorUnpair (cantorUnpair (zfNot φ)).1).2 v else if h3 : (cantorUnpair (zfNot φ)).2 = 3 then have hm := ⋯; ¬zfHolds (cantorUnpair (zfNot φ)).1 v else if h4 : (cantorUnpair (zfNot φ)).2 = 4 then have hm := ⋯; have hp := ⋯; ∀ (s : ZFSet.{u}), zfHolds (cantorUnpair (cantorUnpair (zfNot φ)).1).2 (Function.update v (cantorUnpair (cantorUnpair (zfNot φ)).1).1 s) else True) ↔ ¬zfHolds φ v All goals completed! 🐙@[simp] theorem zfHolds_zfAll (x φ : ℕ) (v : ℕ → ZFSet.{u}) : zfHolds (zfAll x φ) v ↔ ∀ s : ZFSet.{u}, zfHolds φ (Function.update v x s) := x:ℕφ:ℕv:ℕ → ZFSet.{u}⊢ zfHolds (zfAll x φ) v ↔ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update v x s) x:ℕφ:ℕv:ℕ → ZFSet.{u}⊢ (if h0 : (cantorUnpair (zfAll x φ)).2 = 0 then v (cantorUnpair (cantorUnpair (zfAll x φ)).1).1 = v (cantorUnpair (cantorUnpair (zfAll x φ)).1).2 else if h1 : (cantorUnpair (zfAll x φ)).2 = 1 then v (cantorUnpair (cantorUnpair (zfAll x φ)).1).1 ∈ v (cantorUnpair (cantorUnpair (zfAll x φ)).1).2 else if h2 : (cantorUnpair (zfAll x φ)).2 = 2 then have hm := ⋯; have hp := ⋯; have hq := ⋯; zfHolds (cantorUnpair (cantorUnpair (zfAll x φ)).1).1 v → zfHolds (cantorUnpair (cantorUnpair (zfAll x φ)).1).2 v else if h3 : (cantorUnpair (zfAll x φ)).2 = 3 then have hm := ⋯; ¬zfHolds (cantorUnpair (zfAll x φ)).1 v else if h4 : (cantorUnpair (zfAll x φ)).2 = 4 then have hm := ⋯; have hp := ⋯; ∀ (s : ZFSet.{u}), zfHolds (cantorUnpair (cantorUnpair (zfAll x φ)).1).2 (Function.update v (cantorUnpair (cantorUnpair (zfAll x φ)).1).1 s) else True) ↔ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update v x s) All goals completed! 🐙@[simp] theorem zfHolds_zfEx (x φ : ℕ) (v : ℕ → ZFSet.{u}) : zfHolds (zfEx x φ) v ↔ ∃ s : ZFSet.{u}, zfHolds φ (Function.update v x s) := x:ℕφ:ℕv:ℕ → ZFSet.{u}⊢ zfHolds (zfEx x φ) v ↔ ∃ s, zfHolds φ (Function.update v x s) All goals completed! 🐙@[simp] theorem zfHolds_zfAnd (φ ψ : ℕ) (v : ℕ → ZFSet.{u}) : zfHolds (zfAnd φ ψ) v ↔ (zfHolds φ v ∧ zfHolds ψ v) := φ:ℕψ:ℕv:ℕ → ZFSet.{u}⊢ zfHolds (zfAnd φ ψ) v ↔ zfHolds φ v ∧ zfHolds ψ v All goals completed! 🐙

Section 2: Agreement of zfHolds with ZFFormula.Holds

open ZFFormula in @[simp] theorem code_ex (x : ℕ) (φ : ZFFormula) : (ex x φ).code = zfEx x φ.code := rflopen ZFFormula in @[simp] theorem code_and (φ ψ : ZFFormula) : (and φ ψ).code = zfAnd φ.code ψ.code := rflopen ZFFormula in @[simp] theorem holds_ex (v : ℕ → ZFSet.{u}) (x : ℕ) (φ : ZFFormula) : (ex x φ).Holds v ↔ ∃ s : ZFSet.{u}, φ.Holds (Function.update v x s) := v:ℕ → ZFSet.{u}x:ℕφ:ZFFormula⊢ Holds v (ex x φ) ↔ ∃ s, Holds (Function.update v x s) φ All goals completed! 🐙@[simp] theorem holds_and (v : ℕ → ZFSet.{u}) (φ ψ : ZFFormula) : (ZFFormula.and φ ψ).Holds v ↔ φ.Holds v ∧ ψ.Holds v := v:ℕ → ZFSet.{u}φ:ZFFormulaψ:ZFFormula⊢ ZFFormula.Holds v (φ.and ψ) ↔ ZFFormula.Holds v φ ∧ ZFFormula.Holds v ψ All goals completed! 🐙

zfHolds on the Gödel code of any ZFFormula agrees with ZFFormula.Holds.

@[simp] theorem zfHolds_code (φ : ZFFormula) (v : ℕ → ZFSet.{u}) : zfHolds φ.code v ↔ φ.Holds v := φ:ZFFormulav:ℕ → ZFSet.{u}⊢ zfHolds φ.code v ↔ ZFFormula.Holds v φ induction φ generalizing v with x:ℕy:ℕv:ℕ → ZFSet.{u}⊢ zfHolds (ZFFormula.eq x y).code v ↔ ZFFormula.Holds v (ZFFormula.eq x y) All goals completed! 🐙 x:ℕy:ℕv:ℕ → ZFSet.{u}⊢ zfHolds (ZFFormula.mem x y).code v ↔ ZFFormula.Holds v (ZFFormula.mem x y) All goals completed! 🐙 φ:ZFFormulaψ:ZFFormulaihφ:∀ (v : ℕ → ZFSet.{u}), zfHolds φ.code v ↔ ZFFormula.Holds v φihψ:∀ (v : ℕ → ZFSet.{u}), zfHolds ψ.code v ↔ ZFFormula.Holds v ψv:ℕ → ZFSet.{u}⊢ zfHolds (φ.imp ψ).code v ↔ ZFFormula.Holds v (φ.imp ψ) All goals completed! 🐙 φ:ZFFormulaihφ:∀ (v : ℕ → ZFSet.{u}), zfHolds φ.code v ↔ ZFFormula.Holds v φv:ℕ → ZFSet.{u}⊢ zfHolds φ.not.code v ↔ ZFFormula.Holds v φ.not All goals completed! 🐙 x:ℕφ:ZFFormulaihφ:∀ (v : ℕ → ZFSet.{u}), zfHolds φ.code v ↔ ZFFormula.Holds v φv:ℕ → ZFSet.{u}⊢ zfHolds (ZFFormula.all x φ).code v ↔ ZFFormula.Holds v (ZFFormula.all x φ) All goals completed! 🐙

The contradiction formula $v_0 \in v_0$ is refutable in Mathlib's ZFSet.{u} under the empty-set valuation fun _ => ∅.

theorem not_holds_mem_zero_zero : ¬ (ZFFormula.mem 0 0).Holds (fun _ => (∅ : ZFSet.{u})) := ZFSet.notMem_empty ∅

Section 3b: Soundness of ZFProvable in ZFSet

attribute [local instance] Classical.allZFSetDefinableprivate theorem update_rep_lhs (v : ℕ → ZFSet.{u}) (x y z s : ZFSet.{u}) : Function.update (Function.update (Function.update (Function.update v 3 x) 1 y) 2 z) 1 s = Function.update (Function.update (Function.update v 3 x) 2 z) 1 s := v:ℕ → ZFSet.{u}x:ZFSet.{u}y:ZFSet.{u}z:ZFSet.{u}s:ZFSet.{u}⊢ Function.update (Function.update (Function.update (Function.update v 3 x) 1 y) 2 z) 1 s = Function.update (Function.update (Function.update v 3 x) 2 z) 1 s All goals completed! 🐙private theorem update_rep_rhs (v : ℕ → ZFSet.{u}) (B z x s : ZFSet.{u}) : Function.update (Function.update (Function.update (Function.update v 1 B) 2 z) 3 x) 1 s = Function.update (Function.update (Function.update v 3 x) 2 z) 1 s := v:ℕ → ZFSet.{u}B:ZFSet.{u}z:ZFSet.{u}x:ZFSet.{u}s:ZFSet.{u}⊢ Function.update (Function.update (Function.update (Function.update v 1 B) 2 z) 3 x) 1 s = Function.update (Function.update (Function.update v 3 x) 2 z) 1 s All goals completed! 🐙private theorem zfHolds_axRep (φ : ℕ) (v : ℕ → ZFSet.{u}) : zfHolds (axRep φ) v := φ:ℕv:ℕ → ZFSet.{u}⊢ zfHolds (axRep φ) v φ:ℕv:ℕ → ZFSet.{u}⊢ (∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1) → ∃ s, ∀ (s_1 : ZFSet.{u}), (Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1 → ∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) ∧ ((∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) → Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1⊢ ∃ s, ∀ (s_1 : ZFSet.{u}), (Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1 → ∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) ∧ ((∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) → Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = y⊢ ∃ s, ∀ (s_1 : ZFSet.{u}), (Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1 → ∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) ∧ ((∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) → Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = yP:ZFSet.{u} → ZFSet.{u} → Prop := fun x z ↦ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)⊢ ∃ s, ∀ (s_1 : ZFSet.{u}), (Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1 → ∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) ∧ ((∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) → Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = yP:ZFSet.{u} → ZFSet.{u} → Prop := fun x z ↦ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)f:ZFSet.{u} → ZFSet.{u} := fun x ↦ Classical.choose ⋯⊢ ∃ s, ∀ (s_1 : ZFSet.{u}), (Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1 → ∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) ∧ ((∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) → Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = yP:ZFSet.{u} → ZFSet.{u} → Prop := fun x z ↦ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)f:ZFSet.{u} → ZFSet.{u} := fun x ↦ Classical.choose ⋯hf:∀ (x z : ZFSet.{u}), P x z → z = f x⊢ ∃ s, ∀ (s_1 : ZFSet.{u}), (Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1 → ∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) ∧ ((∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) → Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = yP:ZFSet.{u} → ZFSet.{u} → Prop := fun x z ↦ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)f:ZFSet.{u} → ZFSet.{u} := fun x ↦ Classical.choose ⋯hf:∀ (x z : ZFSet.{u}), P x z → z = f xB:ZFSet.{u} := ZFSet.sep (fun z ↦ ∃ x ∈ v 0, P x z) (ZFSet.image f (v 0))⊢ ∃ s, ∀ (s_1 : ZFSet.{u}), (Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1 → ∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) ∧ ((∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0 ∧ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s_2) 2 s_1) 1 s)) → Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = yP:ZFSet.{u} → ZFSet.{u} → Prop := fun x z ↦ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)f:ZFSet.{u} → ZFSet.{u} := fun x ↦ Classical.choose ⋯hf:∀ (x z : ZFSet.{u}), P x z → z = f xB:ZFSet.{u} := ZFSet.sep (fun z ↦ ∃ x ∈ v 0, P x z) (ZFSet.image f (v 0))z:ZFSet.{u}⊢ (Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1 → ∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) ∧ ((∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) → Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = yP:ZFSet.{u} → ZFSet.{u} → Prop := fun x z ↦ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)f:ZFSet.{u} → ZFSet.{u} := fun x ↦ Classical.choose ⋯hf:∀ (x z : ZFSet.{u}), P x z → z = f xB:ZFSet.{u} := ZFSet.sep (fun z ↦ ∃ x ∈ v 0, P x z) (ZFSet.image f (v 0))z:ZFSet.{u}hB:z ∈ B ↔ ∃ x ∈ v 0, P x z⊢ (Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1 → ∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) ∧ ((∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) → Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = yP:ZFSet.{u} → ZFSet.{u} → Prop := fun x z ↦ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)f:ZFSet.{u} → ZFSet.{u} := fun x ↦ Classical.choose ⋯hf:∀ (x z : ZFSet.{u}), P x z → z = f xB:ZFSet.{u} := ZFSet.sep (fun z ↦ ∃ x ∈ v 0, P x z) (ZFSet.image f (v 0))z:ZFSet.{u}hB:z ∈ B ↔ ∃ x ∈ v 0, P x zhv1:Function.update (Function.update v 1 B) 2 z 2 = z⊢ (Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1 → ∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) ∧ ((∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) → Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = yP:ZFSet.{u} → ZFSet.{u} → Prop := fun x z ↦ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)f:ZFSet.{u} → ZFSet.{u} := fun x ↦ Classical.choose ⋯hf:∀ (x z : ZFSet.{u}), P x z → z = f xB:ZFSet.{u} := ZFSet.sep (fun z ↦ ∃ x ∈ v 0, P x z) (ZFSet.image f (v 0))z:ZFSet.{u}hB:z ∈ B ↔ ∃ x ∈ v 0, P x zhv1:Function.update (Function.update v 1 B) 2 z 2 = zhv2:Function.update (Function.update v 1 B) 2 z 1 = B⊢ (Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1 → ∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) ∧ ((∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) → Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = yP:ZFSet.{u} → ZFSet.{u} → Prop := fun x z ↦ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)f:ZFSet.{u} → ZFSet.{u} := fun x ↦ Classical.choose ⋯hf:∀ (x z : ZFSet.{u}), P x z → z = f xB:ZFSet.{u} := ZFSet.sep (fun z ↦ ∃ x ∈ v 0, P x z) (ZFSet.image f (v 0))z:ZFSet.{u}hB:z ∈ B ↔ ∃ x ∈ v 0, P x zhv1:Function.update (Function.update v 1 B) 2 z 2 = zhv2:Function.update (Function.update v 1 B) 2 z 1 = Bhv3:∀ (x : ZFSet.{u}), Function.update (Function.update (Function.update v 1 B) 2 z) 3 x 3 = x⊢ (Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1 → ∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) ∧ ((∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) → Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = yP:ZFSet.{u} → ZFSet.{u} → Prop := fun x z ↦ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)f:ZFSet.{u} → ZFSet.{u} := fun x ↦ Classical.choose ⋯hf:∀ (x z : ZFSet.{u}), P x z → z = f xB:ZFSet.{u} := ZFSet.sep (fun z ↦ ∃ x ∈ v 0, P x z) (ZFSet.image f (v 0))z:ZFSet.{u}hB:z ∈ B ↔ ∃ x ∈ v 0, P x zhv1:Function.update (Function.update v 1 B) 2 z 2 = zhv2:Function.update (Function.update v 1 B) 2 z 1 = Bhv3:∀ (x : ZFSet.{u}), Function.update (Function.update (Function.update v 1 B) 2 z) 3 x 3 = xhv0:∀ (x : ZFSet.{u}), Function.update (Function.update (Function.update v 1 B) 2 z) 3 x 0 = v 0⊢ (Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1 → ∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) ∧ ((∃ s, Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 B) 2 z) 3 s 0 ∧ ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) → Function.update (Function.update v 1 B) 2 z 2 ∈ Function.update (Function.update v 1 B) 2 z 1) φ:ℕv:ℕ → ZFSet.{u}h:∀ (s : ZFSet.{u}), ∃ s_1, ∀ (s_2 : ZFSet.{u}), (∀ (s_3 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 s_2) 1 s_3)) → Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 2 = Function.update (Function.update (Function.update v 3 s) 1 s_1) 2 s_2 1h':∀ (x : ZFSet.{u}), ∃ y, ∀ (z : ZFSet.{u}), (∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)) → z = yP:ZFSet.{u} → ZFSet.{u} → Prop := fun x z ↦ ∀ (s : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 x) 2 z) 1 s)f:ZFSet.{u} → ZFSet.{u} := fun x ↦ Classical.choose ⋯hf:∀ (x z : ZFSet.{u}), P x z → z = f xB:ZFSet.{u} := ZFSet.sep (fun z ↦ ∃ x ∈ v 0, P x z) (ZFSet.image f (v 0))z:ZFSet.{u}hB:z ∈ B ↔ ∃ x ∈ v 0, P x zhv1:Function.update (Function.update v 1 B) 2 z 2 = zhv2:Function.update (Function.update v 1 B) 2 z 1 = Bhv3:∀ (x : ZFSet.{u}), Function.update (Function.update (Function.update v 1 B) 2 z) 3 x 3 = xhv0:∀ (x : ZFSet.{u}), Function.update (Function.update (Function.update v 1 B) 2 z) 3 x 0 = v 0⊢ (z ∈ B → ∃ s ∈ v 0, ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) ∧ ((∃ s ∈ v 0, ∀ (s_1 : ZFSet.{u}), zfHolds φ (Function.update (Function.update (Function.update v 3 s) 2 z) 1 s_1)) → z ∈ B) All goals completed! 🐙

Iterated singleton operation $n \mapsto {\dots{a}\dots}$ used to witness axInf.

def iterSingleton (a : ZFSet.{u}) : ℕ → ZFSet.{u} | 0 => a | n + 1 => {iterSingleton a n}private theorem zfHolds_axInf (v : ℕ → ZFSet.{0}) : zfHolds axInf v := v:ℕ → ZFSet.{0}⊢ zfHolds axInf v v:ℕ → ZFSet.{0}⊢ ∃ s, Function.update v 1 s 0 ∈ Function.update v 1 s 1 ∧ ∀ (s_1 : ZFSet.{0}), Function.update (Function.update v 1 s) 0 s_1 0 ∈ Function.update (Function.update v 1 s) 0 s_1 1 → ∃ s_2, Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2 2 ∈ Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2 1 ∧ ∀ (s_3 : ZFSet.{0}), (Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 2 → Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 1 = Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 1 = Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 0 → Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))⊢ ∃ s, Function.update v 1 s 0 ∈ Function.update v 1 s 1 ∧ ∀ (s_1 : ZFSet.{0}), Function.update (Function.update v 1 s) 0 s_1 0 ∈ Function.update (Function.update v 1 s) 0 s_1 1 → ∃ s_2, Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2 2 ∈ Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2 1 ∧ ∀ (s_3 : ZFSet.{0}), (Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 2 → Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 1 = Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 1 = Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 0 → Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 s) 0 s_1) 2 s_2) 1 s_3 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))⊢ Function.update v 1 W 0 ∈ Function.update v 1 W 1v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))⊢ ∀ (s : ZFSet.{0}), Function.update (Function.update v 1 W) 0 s 0 ∈ Function.update (Function.update v 1 W) 0 s 1 → ∃ s_1, Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1 2 ∈ Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1 1 ∧ ∀ (s_2 : ZFSet.{0}), (Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 2 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 0 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))⊢ Function.update v 1 W 0 ∈ Function.update v 1 W 1 v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))h0:Function.update v 1 W 0 = v 0⊢ Function.update v 1 W 0 ∈ Function.update v 1 W 1 v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))h0:Function.update v 1 W 0 = v 0h1:Function.update v 1 W 1 = W⊢ Function.update v 1 W 0 ∈ Function.update v 1 W 1 v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))h0:Function.update v 1 W 0 = v 0h1:Function.update v 1 W 1 = W⊢ ∃ i, iterSingleton (v 0) i = v 0 All goals completed! 🐙 v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))⊢ ∀ (s : ZFSet.{0}), Function.update (Function.update v 1 W) 0 s 0 ∈ Function.update (Function.update v 1 W) 0 s 1 → ∃ s_1, Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1 2 ∈ Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1 1 ∧ ∀ (s_2 : ZFSet.{0}), (Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 2 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 0 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 s) 2 s_1) 1 s_2 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))x:ZFSet.{0}hx:Function.update (Function.update v 1 W) 0 x 0 ∈ Function.update (Function.update v 1 W) 0 x 1⊢ ∃ s, Function.update (Function.update (Function.update v 1 W) 0 x) 2 s 2 ∈ Function.update (Function.update (Function.update v 1 W) 0 x) 2 s 1 ∧ ∀ (s_1 : ZFSet.{0}), (Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 2 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 0 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))x:ZFSet.{0}hx:Function.update (Function.update v 1 W) 0 x 0 ∈ Function.update (Function.update v 1 W) 0 x 1hxW:x ∈ W⊢ ∃ s, Function.update (Function.update (Function.update v 1 W) 0 x) 2 s 2 ∈ Function.update (Function.update (Function.update v 1 W) 0 x) 2 s 1 ∧ ∀ (s_1 : ZFSet.{0}), (Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 2 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 0 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 x) 2 s) 1 s_1 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ W⊢ ∃ s, Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 s 2 ∈ Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 s 1 ∧ ∀ (s_1 : ZFSet.{0}), (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 s) 1 s_1 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 s) 1 s_1 2 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 s) 1 s_1 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 s) 1 s_1 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 s) 1 s_1 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 s) 1 s_1 0 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 s) 1 s_1 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 s) 1 s_1 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ W⊢ Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 2 ∈ Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 1v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ W⊢ ∀ (s : ZFSet.{0}), (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 2 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 0 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ W⊢ Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 2 ∈ Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 1 v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ Wh2:Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 2 = {iterSingleton (v 0) n}⊢ Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 2 ∈ Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 1 v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ Wh2:Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 2 = {iterSingleton (v 0) n}h1:Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 1 = W⊢ Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 2 ∈ Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 1 v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ Wh2:Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 2 = {iterSingleton (v 0) n}h1:Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n} 1 = W⊢ ∃ i, iterSingleton (v 0) i = {iterSingleton (v 0) n} All goals completed! 🐙 v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ W⊢ ∀ (s : ZFSet.{0}), (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 2 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 0 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 s 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ Wz:ZFSet.{0}⊢ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 2 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 0 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ Wz:ZFSet.{0}hz1:Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = z⊢ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 2 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 0 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ Wz:ZFSet.{0}hz1:Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = zhz2:Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 2 = {iterSingleton (v 0) n}⊢ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 2 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 0 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ Wz:ZFSet.{0}hz1:Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = zhz2:Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 2 = {iterSingleton (v 0) n}hz0:Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 0 = iterSingleton (v 0) n⊢ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 2 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 0) ∧ (Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 0 → Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 ∈ Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 2) v:ℕ → ZFSet.{0}W:ZFSet.{0} := ZFSet.range (iterSingleton (v 0))n:ℕhx:Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 0 ∈ Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n) 1hxW:iterSingleton (v 0) n ∈ Wz:ZFSet.{0}hz1:Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 1 = zhz2:Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 2 = {iterSingleton (v 0) n}hz0:Function.update (Function.update (Function.update (Function.update v 1 W) 0 (iterSingleton (v 0) n)) 2 {iterSingleton (v 0) n}) 1 z 0 = iterSingleton (v 0) n⊢ (z = iterSingleton (v 0) n → z = iterSingleton (v 0) n) ∧ (z = iterSingleton (v 0) n → z = iterSingleton (v 0) n) All goals completed! 🐙

Soundness of ZFProvable with respect to the total Tarski valuation zfHolds on ZFSet.{0}.

theorem zfProvable_zfHolds {n : ℕ} (h : ZFProvable n) (v : ℕ → ZFSet.{0}) : zfHolds n v := n:ℕh:ZFProvable nv:ℕ → ZFSet.{0}⊢ zfHolds n v induction h generalizing v with n:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (zfEq 0 0) v All goals completed! 🐙 n:ℕφ✝:ℕψ✝:ℕa✝¹:ZFProvable φ✝a✝:ZFProvable (zfImp φ✝ ψ✝)ih1:∀ (v : ℕ → ZFSet.{0}), zfHolds φ✝ vih2:∀ (v : ℕ → ZFSet.{0}), zfHolds (zfImp φ✝ ψ✝) vv:ℕ → ZFSet.{0}⊢ zfHolds ψ✝ v All goals completed! 🐙 n:ℕx:ℕφ✝:ℕa✝:ZFProvable φ✝ih:∀ (v : ℕ → ZFSet.{0}), zfHolds φ✝ vv:ℕ → ZFSet.{0}⊢ zfHolds (zfAll x φ✝) v n:ℕx:ℕφ✝:ℕa✝:ZFProvable φ✝ih:∀ (v : ℕ → ZFSet.{0}), zfHolds φ✝ vv:ℕ → ZFSet.{0}⊢ ∀ (s : ZFSet.{0}), zfHolds φ✝ (Function.update v x s) n:ℕx:ℕφ✝:ℕa✝:ZFProvable φ✝ih:∀ (v : ℕ → ZFSet.{0}), zfHolds φ✝ vv:ℕ → ZFSet.{0}s:ZFSet.{0}⊢ zfHolds φ✝ (Function.update v x s) All goals completed! 🐙 n:ℕφ:ℕψ:ℕχ:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (axB1 φ ψ χ) v n:ℕφ:ℕψ:ℕχ:ℕv:ℕ → ZFSet.{0}⊢ (zfHolds φ v → zfHolds ψ v) → (zfHolds ψ v → zfHolds χ v) → zfHolds φ v → zfHolds χ v n:ℕφ:ℕψ:ℕχ:ℕv:ℕ → ZFSet.{0}h1:zfHolds φ v → zfHolds ψ vh2:zfHolds ψ v → zfHolds χ vh3:zfHolds φ v⊢ zfHolds χ v All goals completed! 🐙 n:ℕφ:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (axB2 φ) v n:ℕφ:ℕv:ℕ → ZFSet.{0}⊢ (¬zfHolds φ v → zfHolds φ v) → zfHolds φ v n:ℕφ:ℕv:ℕ → ZFSet.{0}h:¬zfHolds φ v → zfHolds φ v⊢ zfHolds φ v n:ℕφ:ℕv:ℕ → ZFSet.{0}h:¬zfHolds φ v → zfHolds φ vhφ:zfHolds φ v⊢ zfHolds φ vn:ℕφ:ℕv:ℕ → ZFSet.{0}h:¬zfHolds φ v → zfHolds φ vhφ:¬zfHolds φ v⊢ zfHolds φ v n:ℕφ:ℕv:ℕ → ZFSet.{0}h:¬zfHolds φ v → zfHolds φ vhφ:zfHolds φ v⊢ zfHolds φ v All goals completed! 🐙 n:ℕφ:ℕv:ℕ → ZFSet.{0}h:¬zfHolds φ v → zfHolds φ vhφ:¬zfHolds φ v⊢ zfHolds φ v All goals completed! 🐙 n:ℕφ:ℕψ:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (axB3 φ ψ) v n:ℕφ:ℕψ:ℕv:ℕ → ZFSet.{0}⊢ zfHolds φ v → ¬zfHolds φ v → zfHolds ψ v n:ℕφ:ℕψ:ℕv:ℕ → ZFSet.{0}h1:zfHolds φ vh2:¬zfHolds φ v⊢ zfHolds ψ v All goals completed! 🐙 n:ℕx:ℕφ:ℕψ:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (axB4 x φ ψ) v n:ℕx:ℕφ:ℕψ:ℕv:ℕ → ZFSet.{0}⊢ (∀ (s : ZFSet.{0}), zfHolds φ (Function.update v x s) → zfHolds ψ (Function.update v x s)) → (∀ (s : ZFSet.{0}), zfHolds φ (Function.update v x s)) → ∀ (s : ZFSet.{0}), zfHolds ψ (Function.update v x s) n:ℕx:ℕφ:ℕψ:ℕv:ℕ → ZFSet.{0}h1:∀ (s : ZFSet.{0}), zfHolds φ (Function.update v x s) → zfHolds ψ (Function.update v x s)h2:∀ (s : ZFSet.{0}), zfHolds φ (Function.update v x s)s:ZFSet.{0}⊢ zfHolds ψ (Function.update v x s) All goals completed! 🐙 n:ℕx:ℕy:ℕz:ℕhxz:x ≠ zhzy:z ≠ yv:ℕ → ZFSet.{0}⊢ zfHolds (axB6a x y z) v All goals completed! 🐙 n:ℕx:ℕy:ℕφ:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (axB6b x y φ) v n:ℕx:ℕy:ℕφ:ℕv:ℕ → ZFSet.{0}⊢ (∀ (s s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) y s_1)) → ∀ (s s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v y s) x s_1) n:ℕx:ℕy:ℕφ:ℕv:ℕ → ZFSet.{0}h:∀ (s s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) y s_1)t:ZFSet.{0}s:ZFSet.{0}⊢ zfHolds φ (Function.update (Function.update v y t) x s) n:ℕx:ℕy:ℕφ:ℕv:ℕ → ZFSet.{0}h:∀ (s s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) y s_1)t:ZFSet.{0}s:ZFSet.{0}hxy:x = y⊢ zfHolds φ (Function.update (Function.update v y t) x s)n:ℕx:ℕy:ℕφ:ℕv:ℕ → ZFSet.{0}h:∀ (s s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) y s_1)t:ZFSet.{0}s:ZFSet.{0}hxy:¬x = y⊢ zfHolds φ (Function.update (Function.update v y t) x s) n:ℕx:ℕy:ℕφ:ℕv:ℕ → ZFSet.{0}h:∀ (s s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) y s_1)t:ZFSet.{0}s:ZFSet.{0}hxy:x = y⊢ zfHolds φ (Function.update (Function.update v y t) x s) n:ℕx:ℕφ:ℕv:ℕ → ZFSet.{0}t:ZFSet.{0}s:ZFSet.{0}h:∀ (s s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) x s_1)⊢ zfHolds φ (Function.update (Function.update v x t) x s) n:ℕx:ℕφ:ℕv:ℕ → ZFSet.{0}t:ZFSet.{0}s:ZFSet.{0}h:∀ (s s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) x s_1)this:zfHolds φ (Function.update (Function.update v x s) x s)⊢ zfHolds φ (Function.update (Function.update v x t) x s) n:ℕx:ℕφ:ℕv:ℕ → ZFSet.{0}t:ZFSet.{0}s:ZFSet.{0}h:∀ (s s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) x s_1)this:zfHolds φ (Function.update v x s)⊢ zfHolds φ (Function.update v x s) All goals completed! 🐙 n:ℕx:ℕy:ℕφ:ℕv:ℕ → ZFSet.{0}h:∀ (s s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) y s_1)t:ZFSet.{0}s:ZFSet.{0}hxy:¬x = y⊢ zfHolds φ (Function.update (Function.update v y t) x s) n:ℕx:ℕy:ℕφ:ℕv:ℕ → ZFSet.{0}h:∀ (s s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) y s_1)t:ZFSet.{0}s:ZFSet.{0}hxy:¬x = y⊢ zfHolds φ (Function.update (Function.update v x s) y t) All goals completed! 🐙 n:ℕx:ℕφ:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (axB6c x φ) v n:ℕx:ℕφ:ℕv:ℕ → ZFSet.{0}⊢ (∃ s, ∀ (s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) x s_1)) → zfHolds φ v n:ℕx:ℕφ:ℕv:ℕ → ZFSet.{0}s:ZFSet.{0}hs:∀ (s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) x s_1)⊢ zfHolds φ v n:ℕx:ℕφ:ℕv:ℕ → ZFSet.{0}s:ZFSet.{0}hs:∀ (s_1 : ZFSet.{0}), zfHolds φ (Function.update (Function.update v x s) x s_1)this:zfHolds φ (Function.update (Function.update v x s) x (v x))⊢ zfHolds φ v All goals completed! 🐙 n:ℕx:ℕy:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (axB7 x y) v n:ℕx:ℕy:ℕv:ℕ → ZFSet.{0}⊢ ∃ s, Function.update v x s x = Function.update v x s y n:ℕx:ℕy:ℕv:ℕ → ZFSet.{0}⊢ Function.update v x (v y) x = Function.update v x (v y) y n:ℕx:ℕy:ℕv:ℕ → ZFSet.{0}hxy:x = y⊢ Function.update v x (v y) x = Function.update v x (v y) yn:ℕx:ℕy:ℕv:ℕ → ZFSet.{0}hxy:¬x = y⊢ Function.update v x (v y) x = Function.update v x (v y) y n:ℕx:ℕy:ℕv:ℕ → ZFSet.{0}hxy:x = y⊢ Function.update v x (v y) x = Function.update v x (v y) yn:ℕx:ℕy:ℕv:ℕ → ZFSet.{0}hxy:¬x = y⊢ Function.update v x (v y) x = Function.update v x (v y) y All goals completed! 🐙 n:ℕx:ℕy:ℕz:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (axB8a x y z) v n:ℕx:ℕy:ℕz:ℕv:ℕ → ZFSet.{0}⊢ v x = v y → v x = v z → v y = v z n:ℕx:ℕy:ℕz:ℕv:ℕ → ZFSet.{0}h1:v x = v yh2:v x = v z⊢ v y = v z All goals completed! 🐙 n:ℕx:ℕy:ℕz:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (axB8b x y z) v n:ℕx:ℕy:ℕz:ℕv:ℕ → ZFSet.{0}⊢ v x = v y → v x ∈ v z → v y ∈ v z n:ℕx:ℕy:ℕz:ℕv:ℕ → ZFSet.{0}h1:v x = v yh2:v x ∈ v z⊢ v y ∈ v z All goals completed! 🐙 n:ℕx:ℕy:ℕz:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (axB8c x y z) v n:ℕx:ℕy:ℕz:ℕv:ℕ → ZFSet.{0}⊢ v x = v y → v z ∈ v x → v z ∈ v y n:ℕx:ℕy:ℕz:ℕv:ℕ → ZFSet.{0}h1:v x = v yh2:v z ∈ v x⊢ v z ∈ v y All goals completed! 🐙 n:ℕv:ℕ → ZFSet.{0}⊢ zfHolds axExt v n:ℕv:ℕ → ZFSet.{0}⊢ (∀ (s : ZFSet.{0}), (Function.update v 2 s 2 ∈ Function.update v 2 s 0 → Function.update v 2 s 2 ∈ Function.update v 2 s 1) ∧ (Function.update v 2 s 2 ∈ Function.update v 2 s 1 → Function.update v 2 s 2 ∈ Function.update v 2 s 0)) → v 0 = v 1 n:ℕv:ℕ → ZFSet.{0}h:∀ (s : ZFSet.{0}), (Function.update v 2 s 2 ∈ Function.update v 2 s 0 → Function.update v 2 s 2 ∈ Function.update v 2 s 1) ∧ (Function.update v 2 s 2 ∈ Function.update v 2 s 1 → Function.update v 2 s 2 ∈ Function.update v 2 s 0)⊢ v 0 = v 1 n:ℕv:ℕ → ZFSet.{0}h:∀ (s : ZFSet.{0}), (Function.update v 2 s 2 ∈ Function.update v 2 s 0 → Function.update v 2 s 2 ∈ Function.update v 2 s 1) ∧ (Function.update v 2 s 2 ∈ Function.update v 2 s 1 → Function.update v 2 s 2 ∈ Function.update v 2 s 0)⊢ ∀ (z : ZFSet.{0}), z ∈ v 0 ↔ z ∈ v 1 n:ℕv:ℕ → ZFSet.{0}h:∀ (s : ZFSet.{0}), (Function.update v 2 s 2 ∈ Function.update v 2 s 0 → Function.update v 2 s 2 ∈ Function.update v 2 s 1) ∧ (Function.update v 2 s 2 ∈ Function.update v 2 s 1 → Function.update v 2 s 2 ∈ Function.update v 2 s 0)z:ZFSet.{0}⊢ z ∈ v 0 ↔ z ∈ v 1 n:ℕv:ℕ → ZFSet.{0}h:∀ (s : ZFSet.{0}), (Function.update v 2 s 2 ∈ Function.update v 2 s 0 → Function.update v 2 s 2 ∈ Function.update v 2 s 1) ∧ (Function.update v 2 s 2 ∈ Function.update v 2 s 1 → Function.update v 2 s 2 ∈ Function.update v 2 s 0)z:ZFSet.{0}hz:(Function.update v 2 z 2 ∈ Function.update v 2 z 0 → Function.update v 2 z 2 ∈ Function.update v 2 z 1) ∧ (Function.update v 2 z 2 ∈ Function.update v 2 z 1 → Function.update v 2 z 2 ∈ Function.update v 2 z 0)⊢ z ∈ v 0 ↔ z ∈ v 1 All goals completed! 🐙 n:ℕφ:ℕv:ℕ → ZFSet.{0}⊢ zfHolds (axRep φ) v All goals completed! 🐙 n:ℕv:ℕ → ZFSet.{0}⊢ zfHolds axPow v n:ℕv:ℕ → ZFSet.{0}⊢ ∃ s, ∀ (s_1 : ZFSet.{0}), (∀ (s_2 : ZFSet.{0}), Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 2 → Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0) → Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1 n:ℕv:ℕ → ZFSet.{0}z:ZFSet.{0}hz:∀ (s : ZFSet.{0}), Function.update (Function.update (Function.update v 1 (v 0).powerset) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 (v 0).powerset) 2 z) 3 s 2 → Function.update (Function.update (Function.update v 1 (v 0).powerset) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 (v 0).powerset) 2 z) 3 s 0⊢ Function.update (Function.update v 1 (v 0).powerset) 2 z 2 ∈ Function.update (Function.update v 1 (v 0).powerset) 2 z 1 n:ℕv:ℕ → ZFSet.{0}z:ZFSet.{0}hz:∀ (s : ZFSet.{0}), Function.update (Function.update (Function.update v 1 (v 0).powerset) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 (v 0).powerset) 2 z) 3 s 2 → Function.update (Function.update (Function.update v 1 (v 0).powerset) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 (v 0).powerset) 2 z) 3 s 0hz':z ∈ (v 0).powerset⊢ Function.update (Function.update v 1 (v 0).powerset) 2 z 2 ∈ Function.update (Function.update v 1 (v 0).powerset) 2 z 1 All goals completed! 🐙 n:ℕv:ℕ → ZFSet.{0}⊢ zfHolds axUni v n:ℕv:ℕ → ZFSet.{0}⊢ ∃ s, ∀ (s_1 : ZFSet.{0}), (∃ s_2, Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 2 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∧ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 3 ∈ Function.update (Function.update (Function.update v 1 s) 2 s_1) 3 s_2 0) → Function.update (Function.update v 1 s) 2 s_1 2 ∈ Function.update (Function.update v 1 s) 2 s_1 1 n:ℕv:ℕ → ZFSet.{0}z:ZFSet.{0}hz:∃ s, Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 s 2 ∈ Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 s 3 ∧ Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 s 3 ∈ Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 s 0⊢ Function.update (Function.update v 1 (v 0).sUnion) 2 z 2 ∈ Function.update (Function.update v 1 (v 0).sUnion) 2 z 1 n:ℕv:ℕ → ZFSet.{0}z:ZFSet.{0}w:ZFSet.{0}hw1:Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 w 2 ∈ Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 w 3hw2:Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 w 3 ∈ Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 w 0⊢ Function.update (Function.update v 1 (v 0).sUnion) 2 z 2 ∈ Function.update (Function.update v 1 (v 0).sUnion) 2 z 1 n:ℕv:ℕ → ZFSet.{0}z:ZFSet.{0}w:ZFSet.{0}hw1:Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 w 2 ∈ Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 w 3hw2:Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 w 3 ∈ Function.update (Function.update (Function.update v 1 (v 0).sUnion) 2 z) 3 w 0hz':z ∈ (v 0).sUnion⊢ Function.update (Function.update v 1 (v 0).sUnion) 2 z 2 ∈ Function.update (Function.update v 1 (v 0).sUnion) 2 z 1 All goals completed! 🐙 n:ℕv:ℕ → ZFSet.{0}⊢ zfHolds axInf v All goals completed! 🐙

Soundness of the ZFProvable Hilbert system with respect to Mathlib's ZFSet.{0}: any provable well-formed formula holds under every variable assignment v : ℕ → ZFSet.{0}.

theorem zfProvable_sound_zfSet (φ : ZFFormula) (h : ZFProvable φ.code) (v : ℕ → ZFSet.{0}) : φ.Holds v := (zfHolds_code φ v).mp (zfProvable_zfHolds h v)

Relative consistency of ZFProvable from Mathlib's ZFSet.{0} model of ZFC: ZFInconsistent is false assuming zfProvable_sound_zfSet.

theorem not_zfInconsistent : ¬ ZFInconsistent := ⊢ ¬ZFInconsistent h:ZFInconsistent⊢ False h:ZFInconsistenth0:ZFFormula.Holds (fun x ↦ ∅) (ZFFormula.mem 0 0)⊢ False All goals completed! 🐙end ConjectureMachines.Semantics.Zf