Theorem inf2

Description: Variation of Axiom of Infinity. There exists a nonempty set that is a subset of its union (using zfinf as a hypothesis). Abbreviated version of the Axiom of Infinity in FreydScedrov p. 283. (Contributed by NM, 28-Oct-1996)

	Ref	Expression
Hypothesis	inf1.1	|- E. x ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) )
Assertion	inf2	|- E. x ( x =/= (/) /\ x C_ U. x )

Proof

Step	Hyp	Ref	Expression
1		inf1.1	|- E. x ( y e. x /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) )
2	1	inf1	|- E. x ( x =/= (/) /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) )
3		dfss2	|- ( x C_ U. x <-> A. y ( y e. x -> y e. U. x ) )
4		eluni	|- ( y e. U. x <-> E. z ( y e. z /\ z e. x ) )
5	4	imbi2i	|- ( ( y e. x -> y e. U. x ) <-> ( y e. x -> E. z ( y e. z /\ z e. x ) ) )
6	5	albii	|- ( A. y ( y e. x -> y e. U. x ) <-> A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) )
7	3 6	bitri	|- ( x C_ U. x <-> A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) )
8	7	anbi2i	|- ( ( x =/= (/) /\ x C_ U. x ) <-> ( x =/= (/) /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) )
9	8	exbii	|- ( E. x ( x =/= (/) /\ x C_ U. x ) <-> E. x ( x =/= (/) /\ A. y ( y e. x -> E. z ( y e. z /\ z e. x ) ) ) )
10	2 9	mpbir	|- E. x ( x =/= (/) /\ x C_ U. x )