Theorem wfaxinf2

Description: The class of well-founded sets models the Axiom of Infinity ax-inf2 . Part of Corollary II.2.12 of Kunen2 p. 114. (Contributed by Eric Schmidt, 19-Oct-2025)

	Ref	Expression
Hypothesis	wfax.1	|- W = U. ( R1 " On )
Assertion	wfaxinf2	|- E. x e. W ( E. y e. W ( y e. x /\ A. z e. W -. z e. y ) /\ A. y e. W ( y e. x -> E. z e. W ( z e. x /\ A. w e. W ( w e. z <-> ( w e. y \/ w = y ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		wfax.1	|- W = U. ( R1 " On )
2		trwf	|- Tr U. ( R1 " On )
3		treq	|- ( W = U. ( R1 " On ) -> ( Tr W <-> Tr U. ( R1 " On ) ) )
4	1 3	ax-mp	|- ( Tr W <-> Tr U. ( R1 " On ) )
5	2 4	mpbir	|- Tr W
6		onwf	|- On C_ U. ( R1 " On )
7		omelon	|- _om e. On
8	6 7	sselii	|- _om e. U. ( R1 " On )
9	8 1	eleqtrri	|- _om e. W
10		omelaxinf2	|- ( ( Tr W /\ _om e. W ) -> E. x e. W ( E. y e. W ( y e. x /\ A. z e. W -. z e. y ) /\ A. y e. W ( y e. x -> E. z e. W ( z e. x /\ A. w e. W ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) )
11	5 9 10	mp2an	|- E. x e. W ( E. y e. W ( y e. x /\ A. z e. W -. z e. y ) /\ A. y e. W ( y e. x -> E. z e. W ( z e. x /\ A. w e. W ( w e. z <-> ( w e. y \/ w = y ) ) ) ) )