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	⊢ 𝐹 : V –1-1-onto→ V
	permmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
Assertion	permaxinf2	⊢ ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 𝑅 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ( 𝑧 𝑅 𝑥 ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		permmodel.1	⊢ 𝐹 : V –1-1-onto→ V
2		permmodel.2	⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
3		eqid	⊢ ( rec ( ( 𝑣 ∈ V ↦ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑣 ) ∪ { 𝑣 } ) ) ) , ( ◡ 𝐹 ‘ ∅ ) ) “ ω ) = ( rec ( ( 𝑣 ∈ V ↦ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑣 ) ∪ { 𝑣 } ) ) ) , ( ◡ 𝐹 ‘ ∅ ) ) “ ω )
4	1 2 3	permaxinf2lem	⊢ ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 𝑅 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ( 𝑧 𝑅 𝑥 ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )