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 o. _E )
Assertion	permaxinf2	|- E. x ( E. y ( y R x /\ A. z -. z R y ) /\ A. y ( y R x -> E. z ( z R x /\ A. 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 o. _E )
3		eqid	|- ( rec ( ( v e. _V |-> ( `' F ` ( ( F ` v ) u. { v } ) ) ) , ( `' F ` (/) ) ) " _om ) = ( rec ( ( v e. _V |-> ( `' F ` ( ( F ` v ) u. { v } ) ) ) , ( `' F ` (/) ) ) " _om )
4	1 2 3	permaxinf2lem	|- E. x ( E. y ( y R x /\ A. z -. z R y ) /\ A. y ( y R x -> E. z ( z R x /\ A. w ( w R z <-> ( w R y \/ w = y ) ) ) ) )