Metamath Proof Explorer

Theorem permaxinf2

Description: The Axiom of Infinity ax-inf2 holds in permutation models. Part of Exercise II.9.2 of Kunen2 p. 148. (Contributed by Eric Schmidt, 6-Nov-2025)

Ref Expression
Hypotheses permmodel.1 ⊢ F : V ⟶ 1-1 onto V
permmodel.2 ⊢ R = F -1 ∘ E
Assertion permaxinf2 ⊢ ∃ x ∃ y y R x ∧ ∀ z ¬ z R y ∧ ∀ y y R x → ∃ z z R x ∧ ∀ w w R z ↔ w R y ∨ w = y

Proof

Step Hyp Ref Expression
1 permmodel.1 ⊢ F : V ⟶ 1-1 onto V
2 permmodel.2 ⊢ R = F -1 ∘ E
3 eqid ⊢ rec ⁡ v ∈ V ⟼ F -1 ⁡ F ⁡ v ∪ v F -1 ⁡ ∅ ω = rec ⁡ v ∈ V ⟼ F -1 ⁡ F ⁡ v ∪ v F -1 ⁡ ∅ ω
4 1 2 3 permaxinf2lem ⊢ ∃ x ∃ y y R x ∧ ∀ z ¬ z R y ∧ ∀ y y R x → ∃ z z R x ∧ ∀ w w R z ↔ w R y ∨ w = y