This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 df-ss 
 |-  ( 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 )