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

Metamath Proof Explorer

Theorem neiptopuni

Description: Lemma for neiptopreu . (Contributed by Thierry Arnoux, 6-Jan-2018)

Ref Expression
Hypotheses neiptop.o 
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }
neiptop.0 
|- ( ph -> N : X --> ~P ~P X )
neiptop.1 
|- ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )
neiptop.2 
|- ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )
neiptop.3 
|- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )
neiptop.4 
|- ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
neiptop.5 
|- ( ( ph /\ p e. X ) -> X e. ( N ` p ) )
Assertion neiptopuni 
|- ( ph -> X = U. J )

Proof

Step Hyp Ref Expression
1 neiptop.o 
 |-  J = { a e. ~P X | A. p e. a a e. ( N ` p ) }
2 neiptop.0 
 |-  ( ph -> N : X --> ~P ~P X )
3 neiptop.1 
 |-  ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) )
4 neiptop.2 
 |-  ( ( ph /\ p e. X ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )
5 neiptop.3 
 |-  ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a )
6 neiptop.4 
 |-  ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) )
7 neiptop.5 
 |-  ( ( ph /\ p e. X ) -> X e. ( N ` p ) )
8 elpwi 
 |-  ( a e. ~P X -> a C_ X )
9 8 ad2antlr 
 |-  ( ( ( p e. U. J /\ a e. ~P X ) /\ p e. a ) -> a C_ X )
10 simpr 
 |-  ( ( ( p e. U. J /\ a e. ~P X ) /\ p e. a ) -> p e. a )
11 9 10 sseldd 
 |-  ( ( ( p e. U. J /\ a e. ~P X ) /\ p e. a ) -> p e. X )
12 1 unieqi 
 |-  U. J = U. { a e. ~P X | A. p e. a a e. ( N ` p ) }
13 12 eleq2i 
 |-  ( p e. U. J <-> p e. U. { a e. ~P X | A. p e. a a e. ( N ` p ) } )
14 elunirab 
 |-  ( p e. U. { a e. ~P X | A. p e. a a e. ( N ` p ) } <-> E. a e. ~P X ( p e. a /\ A. p e. a a e. ( N ` p ) ) )
15 13 14 bitri 
 |-  ( p e. U. J <-> E. a e. ~P X ( p e. a /\ A. p e. a a e. ( N ` p ) ) )
16 simpl 
 |-  ( ( p e. a /\ A. p e. a a e. ( N ` p ) ) -> p e. a )
17 16 reximi 
 |-  ( E. a e. ~P X ( p e. a /\ A. p e. a a e. ( N ` p ) ) -> E. a e. ~P X p e. a )
18 15 17 sylbi 
 |-  ( p e. U. J -> E. a e. ~P X p e. a )
19 11 18 r19.29a 
 |-  ( p e. U. J -> p e. X )
20 19 a1i 
 |-  ( ph -> ( p e. U. J -> p e. X ) )
21 20 ssrdv 
 |-  ( ph -> U. J C_ X )
22 ssidd 
 |-  ( ph -> X C_ X )
23 7 ralrimiva 
 |-  ( ph -> A. p e. X X e. ( N ` p ) )
24 1 neipeltop 
 |-  ( X e. J <-> ( X C_ X /\ A. p e. X X e. ( N ` p ) ) )
25 22 23 24 sylanbrc 
 |-  ( ph -> X e. J )
26 unissel 
 |-  ( ( U. J C_ X /\ X e. J ) -> U. J = X )
27 21 25 26 syl2anc 
 |-  ( ph -> U. J = X )
28 27 eqcomd 
 |-  ( ph -> X = U. J )