Metamath Proof Explorer

Theorem neiptoptop

Description: Lemma for neiptopreu . (Contributed by Thierry Arnoux, 7-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 neiptoptop 
|- ( ph -> J e. Top )

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 uniss 
 |-  ( e C_ J -> U. e C_ U. J )
9 8 adantl 
 |-  ( ( ph /\ e C_ J ) -> U. e C_ U. J )
10 1 2 3 4 5 6 7 neiptopuni 
 |-  ( ph -> X = U. J )
11 10 adantr 
 |-  ( ( ph /\ e C_ J ) -> X = U. J )
12 9 11 sseqtrrd 
 |-  ( ( ph /\ e C_ J ) -> U. e C_ X )
13 simp-4l 
 |-  ( ( ( ( ( ph /\ e C_ J ) /\ p e. U. e ) /\ c e. e ) /\ p e. c ) -> ph )
14 12 ad3antrrr 
 |-  ( ( ( ( ( ph /\ e C_ J ) /\ p e. U. e ) /\ c e. e ) /\ p e. c ) -> U. e C_ X )
15 simpllr 
 |-  ( ( ( ( ( ph /\ e C_ J ) /\ p e. U. e ) /\ c e. e ) /\ p e. c ) -> p e. U. e )
16 14 15 sseldd 
 |-  ( ( ( ( ( ph /\ e C_ J ) /\ p e. U. e ) /\ c e. e ) /\ p e. c ) -> p e. X )
17 13 16 jca 
 |-  ( ( ( ( ( ph /\ e C_ J ) /\ p e. U. e ) /\ c e. e ) /\ p e. c ) -> ( ph /\ p e. X ) )
18 elssuni 
 |-  ( c e. e -> c C_ U. e )
19 18 ad2antlr 
 |-  ( ( ( ( ( ph /\ e C_ J ) /\ p e. U. e ) /\ c e. e ) /\ p e. c ) -> c C_ U. e )
20 17 19 14 3jca 
 |-  ( ( ( ( ( ph /\ e C_ J ) /\ p e. U. e ) /\ c e. e ) /\ p e. c ) -> ( ( ph /\ p e. X ) /\ c C_ U. e /\ U. e C_ X ) )
21 simpr 
 |-  ( ( ph /\ e C_ J ) -> e C_ J )
22 21 sselda 
 |-  ( ( ( ph /\ e C_ J ) /\ c e. e ) -> c e. J )
23 1 neipeltop 
 |-  ( c e. J <-> ( c C_ X /\ A. p e. c c e. ( N ` p ) ) )
24 23 simprbi 
 |-  ( c e. J -> A. p e. c c e. ( N ` p ) )
25 22 24 syl 
 |-  ( ( ( ph /\ e C_ J ) /\ c e. e ) -> A. p e. c c e. ( N ` p ) )
26 25 r19.21bi 
 |-  ( ( ( ( ph /\ e C_ J ) /\ c e. e ) /\ p e. c ) -> c e. ( N ` p ) )
27 26 adantllr 
 |-  ( ( ( ( ( ph /\ e C_ J ) /\ p e. U. e ) /\ c e. e ) /\ p e. c ) -> c e. ( N ` p ) )
28 sseq1 
 |-  ( a = c -> ( a C_ U. e <-> c C_ U. e ) )
29 28 3anbi2d 
 |-  ( a = c -> ( ( ( ph /\ p e. X ) /\ a C_ U. e /\ U. e C_ X ) <-> ( ( ph /\ p e. X ) /\ c C_ U. e /\ U. e C_ X ) ) )
30 eleq1 
 |-  ( a = c -> ( a e. ( N ` p ) <-> c e. ( N ` p ) ) )
31 29 30 anbi12d 
 |-  ( a = c -> ( ( ( ( ph /\ p e. X ) /\ a C_ U. e /\ U. e C_ X ) /\ a e. ( N ` p ) ) <-> ( ( ( ph /\ p e. X ) /\ c C_ U. e /\ U. e C_ X ) /\ c e. ( N ` p ) ) ) )
32 31 imbi1d 
 |-  ( a = c -> ( ( ( ( ( ph /\ p e. X ) /\ a C_ U. e /\ U. e C_ X ) /\ a e. ( N ` p ) ) -> U. e e. ( N ` p ) ) <-> ( ( ( ( ph /\ p e. X ) /\ c C_ U. e /\ U. e C_ X ) /\ c e. ( N ` p ) ) -> U. e e. ( N ` p ) ) ) )
33 32 imbi2d 
 |-  ( a = c -> ( ( ( ph /\ e C_ J ) -> ( ( ( ( ph /\ p e. X ) /\ a C_ U. e /\ U. e C_ X ) /\ a e. ( N ` p ) ) -> U. e e. ( N ` p ) ) ) <-> ( ( ph /\ e C_ J ) -> ( ( ( ( ph /\ p e. X ) /\ c C_ U. e /\ U. e C_ X ) /\ c e. ( N ` p ) ) -> U. e e. ( N ` p ) ) ) ) )
34 ssidd 
 |-  ( ph -> X C_ X )
35 7 ralrimiva 
 |-  ( ph -> A. p e. X X e. ( N ` p ) )
36 1 neipeltop 
 |-  ( X e. J <-> ( X C_ X /\ A. p e. X X e. ( N ` p ) ) )
37 34 35 36 sylanbrc 
 |-  ( ph -> X e. J )
38 pwexg 
 |-  ( X e. J -> ~P X e. _V )
39 rabexg 
 |-  ( ~P X e. _V -> { a e. ~P X | A. p e. a a e. ( N ` p ) } e. _V )
40 37 38 39 3syl 
 |-  ( ph -> { a e. ~P X | A. p e. a a e. ( N ` p ) } e. _V )
41 1 40 eqeltrid 
 |-  ( ph -> J e. _V )
42 41 adantr 
 |-  ( ( ph /\ e C_ J ) -> J e. _V )
43 42 21 ssexd 
 |-  ( ( ph /\ e C_ J ) -> e e. _V )
44 uniexg 
 |-  ( e e. _V -> U. e e. _V )
45 sseq2 
 |-  ( b = U. e -> ( a C_ b <-> a C_ U. e ) )
46 sseq1 
 |-  ( b = U. e -> ( b C_ X <-> U. e C_ X ) )
47 45 46 3anbi23d 
 |-  ( b = U. e -> ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) <-> ( ( ph /\ p e. X ) /\ a C_ U. e /\ U. e C_ X ) ) )
48 47 anbi1d 
 |-  ( b = U. e -> ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) <-> ( ( ( ph /\ p e. X ) /\ a C_ U. e /\ U. e C_ X ) /\ a e. ( N ` p ) ) ) )
49 eleq1 
 |-  ( b = U. e -> ( b e. ( N ` p ) <-> U. e e. ( N ` p ) ) )
50 48 49 imbi12d 
 |-  ( b = U. e -> ( ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) ) <-> ( ( ( ( ph /\ p e. X ) /\ a C_ U. e /\ U. e C_ X ) /\ a e. ( N ` p ) ) -> U. e e. ( N ` p ) ) ) )
51 50 3 vtoclg 
 |-  ( U. e e. _V -> ( ( ( ( ph /\ p e. X ) /\ a C_ U. e /\ U. e C_ X ) /\ a e. ( N ` p ) ) -> U. e e. ( N ` p ) ) )
52 43 44 51 3syl 
 |-  ( ( ph /\ e C_ J ) -> ( ( ( ( ph /\ p e. X ) /\ a C_ U. e /\ U. e C_ X ) /\ a e. ( N ` p ) ) -> U. e e. ( N ` p ) ) )
53 33 52 chvarvv 
 |-  ( ( ph /\ e C_ J ) -> ( ( ( ( ph /\ p e. X ) /\ c C_ U. e /\ U. e C_ X ) /\ c e. ( N ` p ) ) -> U. e e. ( N ` p ) ) )
54 53 ad3antrrr 
 |-  ( ( ( ( ( ph /\ e C_ J ) /\ p e. U. e ) /\ c e. e ) /\ p e. c ) -> ( ( ( ( ph /\ p e. X ) /\ c C_ U. e /\ U. e C_ X ) /\ c e. ( N ` p ) ) -> U. e e. ( N ` p ) ) )
55 20 27 54 mp2and 
 |-  ( ( ( ( ( ph /\ e C_ J ) /\ p e. U. e ) /\ c e. e ) /\ p e. c ) -> U. e e. ( N ` p ) )
56 simpr 
 |-  ( ( ( ph /\ e C_ J ) /\ p e. U. e ) -> p e. U. e )
57 eluni2 
 |-  ( p e. U. e <-> E. c e. e p e. c )
58 56 57 sylib 
 |-  ( ( ( ph /\ e C_ J ) /\ p e. U. e ) -> E. c e. e p e. c )
59 55 58 r19.29a 
 |-  ( ( ( ph /\ e C_ J ) /\ p e. U. e ) -> U. e e. ( N ` p ) )
60 59 ralrimiva 
 |-  ( ( ph /\ e C_ J ) -> A. p e. U. e U. e e. ( N ` p ) )
61 1 neipeltop 
 |-  ( U. e e. J <-> ( U. e C_ X /\ A. p e. U. e U. e e. ( N ` p ) ) )
62 12 60 61 sylanbrc 
 |-  ( ( ph /\ e C_ J ) -> U. e e. J )
63 62 ex 
 |-  ( ph -> ( e C_ J -> U. e e. J ) )
64 63 alrimiv 
 |-  ( ph -> A. e ( e C_ J -> U. e e. J ) )
65 inss1 
 |-  ( e i^i f ) C_ e
66 1 neipeltop 
 |-  ( e e. J <-> ( e C_ X /\ A. p e. e e e. ( N ` p ) ) )
67 66 simplbi 
 |-  ( e e. J -> e C_ X )
68 67 ad2antlr 
 |-  ( ( ( ph /\ e e. J ) /\ f e. J ) -> e C_ X )
69 65 68 sstrid 
 |-  ( ( ( ph /\ e e. J ) /\ f e. J ) -> ( e i^i f ) C_ X )
70 simplll 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> ph )
71 simpllr 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> e e. J )
72 71 67 syl 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> e C_ X )
73 simpr 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> p e. ( e i^i f ) )
74 73 elin1d 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> p e. e )
75 72 74 sseldd 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> p e. X )
76 70 75 4 syl2anc 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> ( fi ` ( N ` p ) ) C_ ( N ` p ) )
77 fvex 
 |-  ( N ` p ) e. _V
78 66 simprbi 
 |-  ( e e. J -> A. p e. e e e. ( N ` p ) )
79 78 r19.21bi 
 |-  ( ( e e. J /\ p e. e ) -> e e. ( N ` p ) )
80 71 74 79 syl2anc 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> e e. ( N ` p ) )
81 simplr 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> f e. J )
82 73 elin2d 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> p e. f )
83 1 neipeltop 
 |-  ( f e. J <-> ( f C_ X /\ A. p e. f f e. ( N ` p ) ) )
84 83 simprbi 
 |-  ( f e. J -> A. p e. f f e. ( N ` p ) )
85 84 r19.21bi 
 |-  ( ( f e. J /\ p e. f ) -> f e. ( N ` p ) )
86 81 82 85 syl2anc 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> f e. ( N ` p ) )
87 inelfi 
 |-  ( ( ( N ` p ) e. _V /\ e e. ( N ` p ) /\ f e. ( N ` p ) ) -> ( e i^i f ) e. ( fi ` ( N ` p ) ) )
88 77 80 86 87 mp3an2i 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> ( e i^i f ) e. ( fi ` ( N ` p ) ) )
89 76 88 sseldd 
 |-  ( ( ( ( ph /\ e e. J ) /\ f e. J ) /\ p e. ( e i^i f ) ) -> ( e i^i f ) e. ( N ` p ) )
90 89 ralrimiva 
 |-  ( ( ( ph /\ e e. J ) /\ f e. J ) -> A. p e. ( e i^i f ) ( e i^i f ) e. ( N ` p ) )
91 1 neipeltop 
 |-  ( ( e i^i f ) e. J <-> ( ( e i^i f ) C_ X /\ A. p e. ( e i^i f ) ( e i^i f ) e. ( N ` p ) ) )
92 69 90 91 sylanbrc 
 |-  ( ( ( ph /\ e e. J ) /\ f e. J ) -> ( e i^i f ) e. J )
93 92 ralrimiva 
 |-  ( ( ph /\ e e. J ) -> A. f e. J ( e i^i f ) e. J )
94 93 ralrimiva 
 |-  ( ph -> A. e e. J A. f e. J ( e i^i f ) e. J )
95 istopg 
 |-  ( J e. _V -> ( J e. Top <-> ( A. e ( e C_ J -> U. e e. J ) /\ A. e e. J A. f e. J ( e i^i f ) e. J ) ) )
96 41 95 syl 
 |-  ( ph -> ( J e. Top <-> ( A. e ( e C_ J -> U. e e. J ) /\ A. e e. J A. f e. J ( e i^i f ) e. J ) ) )
97 64 94 96 mpbir2and 
 |-  ( ph -> J e. Top )