Theorem axinf2

Description: A standard version of Axiom of Infinity, expanded to primitives, derived from our version of Infinity ax-inf and Regularity ax-reg .

This theorem should not be referenced in any proof. Instead, use ax-inf2 below so that the ordinary uses of Regularity can be more easily identified. (New usage is discouraged.) (Contributed by NM, 3-Nov-1996)

	Ref	Expression
Assertion	axinf2	|- E. x ( E. y ( y e. x /\ A. z -. z e. y ) /\ A. y ( y e. x -> E. z ( z e. x /\ A. w ( w e. z <-> ( w e. y \/ w = y ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		peano1	|- (/) e. _om
2		peano2	|- ( y e. _om -> suc y e. _om )
3	2	ax-gen	|- A. y ( y e. _om -> suc y e. _om )
4		zfinf	|- E. x ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) )
5	4	inf2	|- E. x ( x =/= (/) /\ x C_ U. x )
6	5	inf3	|- _om e. _V
7		eleq2	|- ( x = _om -> ( (/) e. x <-> (/) e. _om ) )
8		eleq2	|- ( x = _om -> ( y e. x <-> y e. _om ) )
9		eleq2	|- ( x = _om -> ( suc y e. x <-> suc y e. _om ) )
10	8 9	imbi12d	|- ( x = _om -> ( ( y e. x -> suc y e. x ) <-> ( y e. _om -> suc y e. _om ) ) )
11	10	albidv	|- ( x = _om -> ( A. y ( y e. x -> suc y e. x ) <-> A. y ( y e. _om -> suc y e. _om ) ) )
12	7 11	anbi12d	|- ( x = _om -> ( ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) ) <-> ( (/) e. _om /\ A. y ( y e. _om -> suc y e. _om ) ) ) )
13	6 12	spcev	|- ( ( (/) e. _om /\ A. y ( y e. _om -> suc y e. _om ) ) -> E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) ) )
14	1 3 13	mp2an	|- E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) )
15		0el	|- ( (/) e. x <-> E. y e. x A. z -. z e. y )
16		df-rex	|- ( E. y e. x A. z -. z e. y <-> E. y ( y e. x /\ A. z -. z e. y ) )
17	15 16	bitri	|- ( (/) e. x <-> E. y ( y e. x /\ A. z -. z e. y ) )
18		sucel	|- ( suc y e. x <-> E. z e. x A. w ( w e. z <-> ( w e. y \/ w = y ) ) )
19		df-rex	|- ( E. z e. x A. w ( w e. z <-> ( w e. y \/ w = y ) ) <-> E. z ( z e. x /\ A. w ( w e. z <-> ( w e. y \/ w = y ) ) ) )
20	18 19	bitri	|- ( suc y e. x <-> E. z ( z e. x /\ A. w ( w e. z <-> ( w e. y \/ w = y ) ) ) )
21	20	imbi2i	|- ( ( y e. x -> suc y e. x ) <-> ( y e. x -> E. z ( z e. x /\ A. w ( w e. z <-> ( w e. y \/ w = y ) ) ) ) )
22	21	albii	|- ( A. y ( y e. x -> suc y e. x ) <-> A. y ( y e. x -> E. z ( z e. x /\ A. w ( w e. z <-> ( w e. y \/ w = y ) ) ) ) )
23	17 22	anbi12i	|- ( ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) ) <-> ( E. y ( y e. x /\ A. z -. z e. y ) /\ A. y ( y e. x -> E. z ( z e. x /\ A. w ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) )
24	23	exbii	|- ( E. x ( (/) e. x /\ A. y ( y e. x -> suc y e. x ) ) <-> E. x ( E. y ( y e. x /\ A. z -. z e. y ) /\ A. y ( y e. x -> E. z ( z e. x /\ A. w ( w e. z <-> ( w e. y \/ w = y ) ) ) ) ) )
25	14 24	mpbi	|- E. x ( E. y ( y e. x /\ A. z -. z e. y ) /\ A. y ( y e. x -> E. z ( z e. x /\ A. w ( w e. z <-> ( w e. y \/ w = y ) ) ) ) )