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

Metamath Proof Explorer

Theorem infeq5i

Description: Half of infeq5 . (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion infeq5i 
|- ( _om e. _V -> E. x x C. U. x )

Proof

Step Hyp Ref Expression
1 difexg 
 |-  ( _om e. _V -> ( _om \ { (/) } ) e. _V )
2 0ex 
 |-  (/) e. _V
3 2 snid 
 |-  (/) e. { (/) }
4 disj4 
 |-  ( ( _om i^i { (/) } ) = (/) <-> -. ( _om \ { (/) } ) C. _om )
5 disj3 
 |-  ( ( _om i^i { (/) } ) = (/) <-> _om = ( _om \ { (/) } ) )
6 4 5 bitr3i 
 |-  ( -. ( _om \ { (/) } ) C. _om <-> _om = ( _om \ { (/) } ) )
7 peano1 
 |-  (/) e. _om
8 eleq2 
 |-  ( _om = ( _om \ { (/) } ) -> ( (/) e. _om <-> (/) e. ( _om \ { (/) } ) ) )
9 7 8 mpbii 
 |-  ( _om = ( _om \ { (/) } ) -> (/) e. ( _om \ { (/) } ) )
10 9 eldifbd 
 |-  ( _om = ( _om \ { (/) } ) -> -. (/) e. { (/) } )
11 6 10 sylbi 
 |-  ( -. ( _om \ { (/) } ) C. _om -> -. (/) e. { (/) } )
12 3 11 mt4 
 |-  ( _om \ { (/) } ) C. _om
13 unidif0 
 |-  U. ( _om \ { (/) } ) = U. _om
14 limom 
 |-  Lim _om
15 limuni 
 |-  ( Lim _om -> _om = U. _om )
16 14 15 ax-mp 
 |-  _om = U. _om
17 13 16 eqtr4i 
 |-  U. ( _om \ { (/) } ) = _om
18 17 psseq2i 
 |-  ( ( _om \ { (/) } ) C. U. ( _om \ { (/) } ) <-> ( _om \ { (/) } ) C. _om )
19 12 18 mpbir 
 |-  ( _om \ { (/) } ) C. U. ( _om \ { (/) } )
20 psseq1 
 |-  ( x = ( _om \ { (/) } ) -> ( x C. U. x <-> ( _om \ { (/) } ) C. U. x ) )
21 unieq 
 |-  ( x = ( _om \ { (/) } ) -> U. x = U. ( _om \ { (/) } ) )
22 21 psseq2d 
 |-  ( x = ( _om \ { (/) } ) -> ( ( _om \ { (/) } ) C. U. x <-> ( _om \ { (/) } ) C. U. ( _om \ { (/) } ) ) )
23 20 22 bitrd 
 |-  ( x = ( _om \ { (/) } ) -> ( x C. U. x <-> ( _om \ { (/) } ) C. U. ( _om \ { (/) } ) ) )
24 23 spcegv 
 |-  ( ( _om \ { (/) } ) e. _V -> ( ( _om \ { (/) } ) C. U. ( _om \ { (/) } ) -> E. x x C. U. x ) )
25 1 19 24 mpisyl 
 |-  ( _om e. _V -> E. x x C. U. x )