Metamath Proof Explorer

Theorem neiptopnei

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 neiptopnei 
|- ( ph -> N = ( p e. X |-> ( ( nei ` J ) ` { p } ) ) )

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 2 feqmptd 
 |-  ( ph -> N = ( p e. X |-> ( N ` p ) ) )
9 2 ffvelrnda 
 |-  ( ( ph /\ p e. X ) -> ( N ` p ) e. ~P ~P X )
10 9 adantr 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> ( N ` p ) e. ~P ~P X )
11 10 elpwid 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> ( N ` p ) C_ ~P X )
12 simpr 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> c e. ( N ` p ) )
13 11 12 sseldd 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> c e. ~P X )
14 13 elpwid 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> c C_ X )
15 1 2 3 4 5 6 7 neiptopuni 
 |-  ( ph -> X = U. J )
16 15 adantr 
 |-  ( ( ph /\ p e. X ) -> X = U. J )
17 16 adantr 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> X = U. J )
18 14 17 sseqtrd 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> c C_ U. J )
19 ssrab2 
 |-  { q e. X | c e. ( N ` q ) } C_ X
20 19 a1i 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> { q e. X | c e. ( N ` q ) } C_ X )
21 fveq2 
 |-  ( q = r -> ( N ` q ) = ( N ` r ) )
22 21 eleq2d 
 |-  ( q = r -> ( c e. ( N ` q ) <-> c e. ( N ` r ) ) )
23 22 elrab 
 |-  ( r e. { q e. X | c e. ( N ` q ) } <-> ( r e. X /\ c e. ( N ` r ) ) )
24 simp-5l 
 |-  ( ( ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( r e. X /\ c e. ( N ` r ) ) ) /\ b e. ( N ` r ) ) /\ b C_ { q e. X | c e. ( N ` q ) } ) -> ph )
25 simpr1l 
 |-  ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( ( r e. X /\ c e. ( N ` r ) ) /\ b e. ( N ` r ) /\ b C_ { q e. X | c e. ( N ` q ) } ) ) -> r e. X )
26 25 3anassrs 
 |-  ( ( ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( r e. X /\ c e. ( N ` r ) ) ) /\ b e. ( N ` r ) ) /\ b C_ { q e. X | c e. ( N ` q ) } ) -> r e. X )
27 simpr 
 |-  ( ( ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( r e. X /\ c e. ( N ` r ) ) ) /\ b e. ( N ` r ) ) /\ b C_ { q e. X | c e. ( N ` q ) } ) -> b C_ { q e. X | c e. ( N ` q ) } )
28 simplr 
 |-  ( ( ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( r e. X /\ c e. ( N ` r ) ) ) /\ b e. ( N ` r ) ) /\ b C_ { q e. X | c e. ( N ` q ) } ) -> b e. ( N ` r ) )
29 sseq1 
 |-  ( a = b -> ( a C_ { q e. X | c e. ( N ` q ) } <-> b C_ { q e. X | c e. ( N ` q ) } ) )
30 29 3anbi2d 
 |-  ( a = b -> ( ( ( ph /\ r e. X ) /\ a C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) <-> ( ( ph /\ r e. X ) /\ b C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) ) )
31 eleq1w 
 |-  ( a = b -> ( a e. ( N ` r ) <-> b e. ( N ` r ) ) )
32 30 31 anbi12d 
 |-  ( a = b -> ( ( ( ( ph /\ r e. X ) /\ a C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) /\ a e. ( N ` r ) ) <-> ( ( ( ph /\ r e. X ) /\ b C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) /\ b e. ( N ` r ) ) ) )
33 32 imbi1d 
 |-  ( a = b -> ( ( ( ( ( ph /\ r e. X ) /\ a C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) /\ a e. ( N ` r ) ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) ) <-> ( ( ( ( ph /\ r e. X ) /\ b C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) /\ b e. ( N ` r ) ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) ) ) )
34 simpl1l 
 |-  ( ( ( ( ph /\ r e. X ) /\ a C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) /\ a e. ( N ` r ) ) -> ph )
35 1 2 3 4 5 6 7 neiptoptop 
 |-  ( ph -> J e. Top )
36 35 uniexd 
 |-  ( ph -> U. J e. _V )
37 15 36 eqeltrd 
 |-  ( ph -> X e. _V )
38 rabexg 
 |-  ( X e. _V -> { q e. X | c e. ( N ` q ) } e. _V )
39 sseq2 
 |-  ( b = { q e. X | c e. ( N ` q ) } -> ( a C_ b <-> a C_ { q e. X | c e. ( N ` q ) } ) )
40 sseq1 
 |-  ( b = { q e. X | c e. ( N ` q ) } -> ( b C_ X <-> { q e. X | c e. ( N ` q ) } C_ X ) )
41 39 40 3anbi23d 
 |-  ( b = { q e. X | c e. ( N ` q ) } -> ( ( ( ph /\ r e. X ) /\ a C_ b /\ b C_ X ) <-> ( ( ph /\ r e. X ) /\ a C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) ) )
42 41 anbi1d 
 |-  ( b = { q e. X | c e. ( N ` q ) } -> ( ( ( ( ph /\ r e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` r ) ) <-> ( ( ( ph /\ r e. X ) /\ a C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) /\ a e. ( N ` r ) ) ) )
43 eleq1 
 |-  ( b = { q e. X | c e. ( N ` q ) } -> ( b e. ( N ` r ) <-> { q e. X | c e. ( N ` q ) } e. ( N ` r ) ) )
44 42 43 imbi12d 
 |-  ( b = { q e. X | c e. ( N ` q ) } -> ( ( ( ( ( ph /\ r e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` r ) ) -> b e. ( N ` r ) ) <-> ( ( ( ( ph /\ r e. X ) /\ a C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) /\ a e. ( N ` r ) ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) ) ) )
45 eleq1w 
 |-  ( p = r -> ( p e. X <-> r e. X ) )
46 45 anbi2d 
 |-  ( p = r -> ( ( ph /\ p e. X ) <-> ( ph /\ r e. X ) ) )
47 46 3anbi1d 
 |-  ( p = r -> ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) <-> ( ( ph /\ r e. X ) /\ a C_ b /\ b C_ X ) ) )
48 fveq2 
 |-  ( p = r -> ( N ` p ) = ( N ` r ) )
49 48 eleq2d 
 |-  ( p = r -> ( a e. ( N ` p ) <-> a e. ( N ` r ) ) )
50 47 49 anbi12d 
 |-  ( p = r -> ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) <-> ( ( ( ph /\ r e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` r ) ) ) )
51 48 eleq2d 
 |-  ( p = r -> ( b e. ( N ` p ) <-> b e. ( N ` r ) ) )
52 50 51 imbi12d 
 |-  ( p = r -> ( ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) ) <-> ( ( ( ( ph /\ r e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` r ) ) -> b e. ( N ` r ) ) ) )
53 52 3 chvarvv 
 |-  ( ( ( ( ph /\ r e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` r ) ) -> b e. ( N ` r ) )
54 44 53 vtoclg 
 |-  ( { q e. X | c e. ( N ` q ) } e. _V -> ( ( ( ( ph /\ r e. X ) /\ a C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) /\ a e. ( N ` r ) ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) ) )
55 37 38 54 3syl 
 |-  ( ph -> ( ( ( ( ph /\ r e. X ) /\ a C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) /\ a e. ( N ` r ) ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) ) )
56 34 55 mpcom 
 |-  ( ( ( ( ph /\ r e. X ) /\ a C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) /\ a e. ( N ` r ) ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) )
57 33 56 chvarvv 
 |-  ( ( ( ( ph /\ r e. X ) /\ b C_ { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ X ) /\ b e. ( N ` r ) ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) )
58 57 3an1rs 
 |-  ( ( ( ( ph /\ r e. X ) /\ b C_ { q e. X | c e. ( N ` q ) } /\ b e. ( N ` r ) ) /\ { q e. X | c e. ( N ` q ) } C_ X ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) )
59 19 58 mpan2 
 |-  ( ( ( ph /\ r e. X ) /\ b C_ { q e. X | c e. ( N ` q ) } /\ b e. ( N ` r ) ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) )
60 24 26 27 28 59 syl211anc 
 |-  ( ( ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( r e. X /\ c e. ( N ` r ) ) ) /\ b e. ( N ` r ) ) /\ b C_ { q e. X | c e. ( N ` q ) } ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) )
61 simplll 
 |-  ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( r e. X /\ c e. ( N ` r ) ) ) -> ph )
62 simprl 
 |-  ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( r e. X /\ c e. ( N ` r ) ) ) -> r e. X )
63 simprr 
 |-  ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( r e. X /\ c e. ( N ` r ) ) ) -> c e. ( N ` r ) )
64 48 eleq2d 
 |-  ( p = r -> ( c e. ( N ` p ) <-> c e. ( N ` r ) ) )
65 46 64 anbi12d 
 |-  ( p = r -> ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) <-> ( ( ph /\ r e. X ) /\ c e. ( N ` r ) ) ) )
66 fveq2 
 |-  ( q = s -> ( N ` q ) = ( N ` s ) )
67 66 eleq2d 
 |-  ( q = s -> ( c e. ( N ` q ) <-> c e. ( N ` s ) ) )
68 67 cbvralvw 
 |-  ( A. q e. b c e. ( N ` q ) <-> A. s e. b c e. ( N ` s ) )
69 68 a1i 
 |-  ( p = r -> ( A. q e. b c e. ( N ` q ) <-> A. s e. b c e. ( N ` s ) ) )
70 48 69 rexeqbidv 
 |-  ( p = r -> ( E. b e. ( N ` p ) A. q e. b c e. ( N ` q ) <-> E. b e. ( N ` r ) A. s e. b c e. ( N ` s ) ) )
71 65 70 imbi12d 
 |-  ( p = r -> ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b c e. ( N ` q ) ) <-> ( ( ( ph /\ r e. X ) /\ c e. ( N ` r ) ) -> E. b e. ( N ` r ) A. s e. b c e. ( N ` s ) ) ) )
72 eleq1w 
 |-  ( a = c -> ( a e. ( N ` p ) <-> c e. ( N ` p ) ) )
73 72 anbi2d 
 |-  ( a = c -> ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) <-> ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) ) )
74 eleq1w 
 |-  ( a = c -> ( a e. ( N ` q ) <-> c e. ( N ` q ) ) )
75 74 rexralbidv 
 |-  ( a = c -> ( E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) <-> E. b e. ( N ` p ) A. q e. b c e. ( N ` q ) ) )
76 73 75 imbi12d 
 |-  ( a = c -> ( ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b a e. ( N ` q ) ) <-> ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b c e. ( N ` q ) ) ) )
77 76 6 chvarvv 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> E. b e. ( N ` p ) A. q e. b c e. ( N ` q ) )
78 71 77 chvarvv 
 |-  ( ( ( ph /\ r e. X ) /\ c e. ( N ` r ) ) -> E. b e. ( N ` r ) A. s e. b c e. ( N ` s ) )
79 2 ffvelrnda 
 |-  ( ( ph /\ r e. X ) -> ( N ` r ) e. ~P ~P X )
80 79 elpwid 
 |-  ( ( ph /\ r e. X ) -> ( N ` r ) C_ ~P X )
81 80 sselda 
 |-  ( ( ( ph /\ r e. X ) /\ b e. ( N ` r ) ) -> b e. ~P X )
82 81 elpwid 
 |-  ( ( ( ph /\ r e. X ) /\ b e. ( N ` r ) ) -> b C_ X )
83 82 sselda 
 |-  ( ( ( ( ph /\ r e. X ) /\ b e. ( N ` r ) ) /\ s e. b ) -> s e. X )
84 83 a1d 
 |-  ( ( ( ( ph /\ r e. X ) /\ b e. ( N ` r ) ) /\ s e. b ) -> ( c e. ( N ` s ) -> s e. X ) )
85 84 ancrd 
 |-  ( ( ( ( ph /\ r e. X ) /\ b e. ( N ` r ) ) /\ s e. b ) -> ( c e. ( N ` s ) -> ( s e. X /\ c e. ( N ` s ) ) ) )
86 85 ralimdva 
 |-  ( ( ( ph /\ r e. X ) /\ b e. ( N ` r ) ) -> ( A. s e. b c e. ( N ` s ) -> A. s e. b ( s e. X /\ c e. ( N ` s ) ) ) )
87 86 reximdva 
 |-  ( ( ph /\ r e. X ) -> ( E. b e. ( N ` r ) A. s e. b c e. ( N ` s ) -> E. b e. ( N ` r ) A. s e. b ( s e. X /\ c e. ( N ` s ) ) ) )
88 87 adantr 
 |-  ( ( ( ph /\ r e. X ) /\ c e. ( N ` r ) ) -> ( E. b e. ( N ` r ) A. s e. b c e. ( N ` s ) -> E. b e. ( N ` r ) A. s e. b ( s e. X /\ c e. ( N ` s ) ) ) )
89 78 88 mpd 
 |-  ( ( ( ph /\ r e. X ) /\ c e. ( N ` r ) ) -> E. b e. ( N ` r ) A. s e. b ( s e. X /\ c e. ( N ` s ) ) )
90 67 elrab 
 |-  ( s e. { q e. X | c e. ( N ` q ) } <-> ( s e. X /\ c e. ( N ` s ) ) )
91 90 ralbii 
 |-  ( A. s e. b s e. { q e. X | c e. ( N ` q ) } <-> A. s e. b ( s e. X /\ c e. ( N ` s ) ) )
92 91 rexbii 
 |-  ( E. b e. ( N ` r ) A. s e. b s e. { q e. X | c e. ( N ` q ) } <-> E. b e. ( N ` r ) A. s e. b ( s e. X /\ c e. ( N ` s ) ) )
93 89 92 sylibr 
 |-  ( ( ( ph /\ r e. X ) /\ c e. ( N ` r ) ) -> E. b e. ( N ` r ) A. s e. b s e. { q e. X | c e. ( N ` q ) } )
94 dfss3 
 |-  ( b C_ { q e. X | c e. ( N ` q ) } <-> A. s e. b s e. { q e. X | c e. ( N ` q ) } )
95 94 biimpri 
 |-  ( A. s e. b s e. { q e. X | c e. ( N ` q ) } -> b C_ { q e. X | c e. ( N ` q ) } )
96 95 reximi 
 |-  ( E. b e. ( N ` r ) A. s e. b s e. { q e. X | c e. ( N ` q ) } -> E. b e. ( N ` r ) b C_ { q e. X | c e. ( N ` q ) } )
97 93 96 syl 
 |-  ( ( ( ph /\ r e. X ) /\ c e. ( N ` r ) ) -> E. b e. ( N ` r ) b C_ { q e. X | c e. ( N ` q ) } )
98 61 62 63 97 syl21anc 
 |-  ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( r e. X /\ c e. ( N ` r ) ) ) -> E. b e. ( N ` r ) b C_ { q e. X | c e. ( N ` q ) } )
99 60 98 r19.29a 
 |-  ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( r e. X /\ c e. ( N ` r ) ) ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) )
100 23 99 sylan2b 
 |-  ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ r e. { q e. X | c e. ( N ` q ) } ) -> { q e. X | c e. ( N ` q ) } e. ( N ` r ) )
101 100 ralrimiva 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> A. r e. { q e. X | c e. ( N ` q ) } { q e. X | c e. ( N ` q ) } e. ( N ` r ) )
102 48 eleq2d 
 |-  ( p = r -> ( { q e. X | c e. ( N ` q ) } e. ( N ` p ) <-> { q e. X | c e. ( N ` q ) } e. ( N ` r ) ) )
103 102 cbvralvw 
 |-  ( A. p e. { q e. X | c e. ( N ` q ) } { q e. X | c e. ( N ` q ) } e. ( N ` p ) <-> A. r e. { q e. X | c e. ( N ` q ) } { q e. X | c e. ( N ` q ) } e. ( N ` r ) )
104 101 103 sylibr 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> A. p e. { q e. X | c e. ( N ` q ) } { q e. X | c e. ( N ` q ) } e. ( N ` p ) )
105 1 neipeltop 
 |-  ( { q e. X | c e. ( N ` q ) } e. J <-> ( { q e. X | c e. ( N ` q ) } C_ X /\ A. p e. { q e. X | c e. ( N ` q ) } { q e. X | c e. ( N ` q ) } e. ( N ` p ) ) )
106 20 104 105 sylanbrc 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> { q e. X | c e. ( N ` q ) } e. J )
107 simpr 
 |-  ( ( ph /\ p e. X ) -> p e. X )
108 107 anim1i 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> ( p e. X /\ c e. ( N ` p ) ) )
109 fveq2 
 |-  ( q = p -> ( N ` q ) = ( N ` p ) )
110 109 eleq2d 
 |-  ( q = p -> ( c e. ( N ` q ) <-> c e. ( N ` p ) ) )
111 110 elrab 
 |-  ( p e. { q e. X | c e. ( N ` q ) } <-> ( p e. X /\ c e. ( N ` p ) ) )
112 108 111 sylibr 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> p e. { q e. X | c e. ( N ` q ) } )
113 nfv 
 |-  F/ q ( ( ph /\ p e. X ) /\ c e. ( N ` p ) )
114 nfrab1 
 |-  F/_ q { q e. X | c e. ( N ` q ) }
115 nfcv 
 |-  F/_ q c
116 rabid 
 |-  ( q e. { q e. X | c e. ( N ` q ) } <-> ( q e. X /\ c e. ( N ` q ) ) )
117 simplll 
 |-  ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( q e. X /\ c e. ( N ` q ) ) ) -> ph )
118 simprl 
 |-  ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( q e. X /\ c e. ( N ` q ) ) ) -> q e. X )
119 simprr 
 |-  ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( q e. X /\ c e. ( N ` q ) ) ) -> c e. ( N ` q ) )
120 eleq1w 
 |-  ( p = q -> ( p e. X <-> q e. X ) )
121 120 anbi2d 
 |-  ( p = q -> ( ( ph /\ p e. X ) <-> ( ph /\ q e. X ) ) )
122 fveq2 
 |-  ( p = q -> ( N ` p ) = ( N ` q ) )
123 122 eleq2d 
 |-  ( p = q -> ( c e. ( N ` p ) <-> c e. ( N ` q ) ) )
124 121 123 anbi12d 
 |-  ( p = q -> ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) <-> ( ( ph /\ q e. X ) /\ c e. ( N ` q ) ) ) )
125 elequ1 
 |-  ( p = q -> ( p e. c <-> q e. c ) )
126 124 125 imbi12d 
 |-  ( p = q -> ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> p e. c ) <-> ( ( ( ph /\ q e. X ) /\ c e. ( N ` q ) ) -> q e. c ) ) )
127 elequ2 
 |-  ( a = c -> ( p e. a <-> p e. c ) )
128 73 127 imbi12d 
 |-  ( a = c -> ( ( ( ( ph /\ p e. X ) /\ a e. ( N ` p ) ) -> p e. a ) <-> ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> p e. c ) ) )
129 128 5 chvarvv 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> p e. c )
130 126 129 chvarvv 
 |-  ( ( ( ph /\ q e. X ) /\ c e. ( N ` q ) ) -> q e. c )
131 117 118 119 130 syl21anc 
 |-  ( ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) /\ ( q e. X /\ c e. ( N ` q ) ) ) -> q e. c )
132 131 ex 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> ( ( q e. X /\ c e. ( N ` q ) ) -> q e. c ) )
133 116 132 syl5bi 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> ( q e. { q e. X | c e. ( N ` q ) } -> q e. c ) )
134 113 114 115 133 ssrd 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> { q e. X | c e. ( N ` q ) } C_ c )
135 eleq2 
 |-  ( d = { q e. X | c e. ( N ` q ) } -> ( p e. d <-> p e. { q e. X | c e. ( N ` q ) } ) )
136 sseq1 
 |-  ( d = { q e. X | c e. ( N ` q ) } -> ( d C_ c <-> { q e. X | c e. ( N ` q ) } C_ c ) )
137 135 136 anbi12d 
 |-  ( d = { q e. X | c e. ( N ` q ) } -> ( ( p e. d /\ d C_ c ) <-> ( p e. { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ c ) ) )
138 137 rspcev 
 |-  ( ( { q e. X | c e. ( N ` q ) } e. J /\ ( p e. { q e. X | c e. ( N ` q ) } /\ { q e. X | c e. ( N ` q ) } C_ c ) ) -> E. d e. J ( p e. d /\ d C_ c ) )
139 106 112 134 138 syl12anc 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> E. d e. J ( p e. d /\ d C_ c ) )
140 18 139 jca 
 |-  ( ( ( ph /\ p e. X ) /\ c e. ( N ` p ) ) -> ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) )
141 nfv 
 |-  F/ d ( ph /\ p e. X )
142 nfv 
 |-  F/ d c C_ U. J
143 nfre1 
 |-  F/ d E. d e. J ( p e. d /\ d C_ c )
144 142 143 nfan 
 |-  F/ d ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) )
145 141 144 nfan 
 |-  F/ d ( ( ph /\ p e. X ) /\ ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) )
146 simplll 
 |-  ( ( ( ( ( ph /\ p e. X ) /\ ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) /\ d e. ( N ` p ) ) /\ d C_ c ) -> ( ph /\ p e. X ) )
147 simpr 
 |-  ( ( ( ( ( ph /\ p e. X ) /\ ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) /\ d e. ( N ` p ) ) /\ d C_ c ) -> d C_ c )
148 simpr1l 
 |-  ( ( ( ph /\ p e. X ) /\ ( ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) /\ d e. ( N ` p ) /\ d C_ c ) ) -> c C_ U. J )
149 148 3anassrs 
 |-  ( ( ( ( ( ph /\ p e. X ) /\ ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) /\ d e. ( N ` p ) ) /\ d C_ c ) -> c C_ U. J )
150 146 16 syl 
 |-  ( ( ( ( ( ph /\ p e. X ) /\ ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) /\ d e. ( N ` p ) ) /\ d C_ c ) -> X = U. J )
151 149 150 sseqtrrd 
 |-  ( ( ( ( ( ph /\ p e. X ) /\ ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) /\ d e. ( N ` p ) ) /\ d C_ c ) -> c C_ X )
152 simplr 
 |-  ( ( ( ( ( ph /\ p e. X ) /\ ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) /\ d e. ( N ` p ) ) /\ d C_ c ) -> d e. ( N ` p ) )
153 sseq1 
 |-  ( a = d -> ( a C_ c <-> d C_ c ) )
154 153 3anbi2d 
 |-  ( a = d -> ( ( ( ph /\ p e. X ) /\ a C_ c /\ c C_ X ) <-> ( ( ph /\ p e. X ) /\ d C_ c /\ c C_ X ) ) )
155 eleq1w 
 |-  ( a = d -> ( a e. ( N ` p ) <-> d e. ( N ` p ) ) )
156 154 155 anbi12d 
 |-  ( a = d -> ( ( ( ( ph /\ p e. X ) /\ a C_ c /\ c C_ X ) /\ a e. ( N ` p ) ) <-> ( ( ( ph /\ p e. X ) /\ d C_ c /\ c C_ X ) /\ d e. ( N ` p ) ) ) )
157 156 imbi1d 
 |-  ( a = d -> ( ( ( ( ( ph /\ p e. X ) /\ a C_ c /\ c C_ X ) /\ a e. ( N ` p ) ) -> c e. ( N ` p ) ) <-> ( ( ( ( ph /\ p e. X ) /\ d C_ c /\ c C_ X ) /\ d e. ( N ` p ) ) -> c e. ( N ` p ) ) ) )
158 sseq2 
 |-  ( b = c -> ( a C_ b <-> a C_ c ) )
159 sseq1 
 |-  ( b = c -> ( b C_ X <-> c C_ X ) )
160 158 159 3anbi23d 
 |-  ( b = c -> ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) <-> ( ( ph /\ p e. X ) /\ a C_ c /\ c C_ X ) ) )
161 160 anbi1d 
 |-  ( b = c -> ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) <-> ( ( ( ph /\ p e. X ) /\ a C_ c /\ c C_ X ) /\ a e. ( N ` p ) ) ) )
162 eleq1w 
 |-  ( b = c -> ( b e. ( N ` p ) <-> c e. ( N ` p ) ) )
163 161 162 imbi12d 
 |-  ( b = c -> ( ( ( ( ( ph /\ p e. X ) /\ a C_ b /\ b C_ X ) /\ a e. ( N ` p ) ) -> b e. ( N ` p ) ) <-> ( ( ( ( ph /\ p e. X ) /\ a C_ c /\ c C_ X ) /\ a e. ( N ` p ) ) -> c e. ( N ` p ) ) ) )
164 163 3 chvarvv 
 |-  ( ( ( ( ph /\ p e. X ) /\ a C_ c /\ c C_ X ) /\ a e. ( N ` p ) ) -> c e. ( N ` p ) )
165 157 164 chvarvv 
 |-  ( ( ( ( ph /\ p e. X ) /\ d C_ c /\ c C_ X ) /\ d e. ( N ` p ) ) -> c e. ( N ` p ) )
166 146 147 151 152 165 syl31anc 
 |-  ( ( ( ( ( ph /\ p e. X ) /\ ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) /\ d e. ( N ` p ) ) /\ d C_ c ) -> c e. ( N ` p ) )
167 1 neipeltop 
 |-  ( d e. J <-> ( d C_ X /\ A. p e. d d e. ( N ` p ) ) )
168 167 simprbi 
 |-  ( d e. J -> A. p e. d d e. ( N ` p ) )
169 168 r19.21bi 
 |-  ( ( d e. J /\ p e. d ) -> d e. ( N ` p ) )
170 169 anim1i 
 |-  ( ( ( d e. J /\ p e. d ) /\ d C_ c ) -> ( d e. ( N ` p ) /\ d C_ c ) )
171 170 anasss 
 |-  ( ( d e. J /\ ( p e. d /\ d C_ c ) ) -> ( d e. ( N ` p ) /\ d C_ c ) )
172 171 reximi2 
 |-  ( E. d e. J ( p e. d /\ d C_ c ) -> E. d e. ( N ` p ) d C_ c )
173 172 ad2antll 
 |-  ( ( ( ph /\ p e. X ) /\ ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) -> E. d e. ( N ` p ) d C_ c )
174 145 166 173 r19.29af 
 |-  ( ( ( ph /\ p e. X ) /\ ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) -> c e. ( N ` p ) )
175 140 174 impbida 
 |-  ( ( ph /\ p e. X ) -> ( c e. ( N ` p ) <-> ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) )
176 107 16 eleqtrd 
 |-  ( ( ph /\ p e. X ) -> p e. U. J )
177 eqid 
 |-  U. J = U. J
178 177 isneip 
 |-  ( ( J e. Top /\ p e. U. J ) -> ( c e. ( ( nei ` J ) ` { p } ) <-> ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) )
179 35 176 178 syl2an2r 
 |-  ( ( ph /\ p e. X ) -> ( c e. ( ( nei ` J ) ` { p } ) <-> ( c C_ U. J /\ E. d e. J ( p e. d /\ d C_ c ) ) ) )
180 175 179 bitr4d 
 |-  ( ( ph /\ p e. X ) -> ( c e. ( N ` p ) <-> c e. ( ( nei ` J ) ` { p } ) ) )
181 180 eqrdv 
 |-  ( ( ph /\ p e. X ) -> ( N ` p ) = ( ( nei ` J ) ` { p } ) )
182 181 mpteq2dva 
 |-  ( ph -> ( p e. X |-> ( N ` p ) ) = ( p e. X |-> ( ( nei ` J ) ` { p } ) ) )
183 8 182 eqtrd 
 |-  ( ph -> N = ( p e. X |-> ( ( nei ` J ) ` { p } ) ) )