Metamath Proof Explorer

Theorem neibastop1

Description: A collection of neighborhood bases determines a topology. Part of Theorem 4.5 of Stephen Willard'sGeneral Topology. (Contributed by Jeff Hankins, 8-Sep-2009) (Proof shortened by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses neibastop1.1 
|- ( ph -> X e. V )
neibastop1.2 
|- ( ph -> F : X --> ( ~P ~P X \ { (/) } ) )
neibastop1.3 
|- ( ( ph /\ ( x e. X /\ v e. ( F ` x ) /\ w e. ( F ` x ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )
neibastop1.4 
|- J = { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) }
Assertion neibastop1 
|- ( ph -> J e. ( TopOn ` X ) )

Proof

Step Hyp Ref Expression
1 neibastop1.1 
 |-  ( ph -> X e. V )
2 neibastop1.2 
 |-  ( ph -> F : X --> ( ~P ~P X \ { (/) } ) )
3 neibastop1.3 
 |-  ( ( ph /\ ( x e. X /\ v e. ( F ` x ) /\ w e. ( F ` x ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )
4 neibastop1.4 
 |-  J = { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) }
5 simpr 
 |-  ( ( ph /\ y C_ J ) -> y C_ J )
6 ssrab2 
 |-  { o e. ~P X | A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) } C_ ~P X
7 4 6 eqsstri 
 |-  J C_ ~P X
8 5 7 sstrdi 
 |-  ( ( ph /\ y C_ J ) -> y C_ ~P X )
9 sspwuni 
 |-  ( y C_ ~P X <-> U. y C_ X )
10 8 9 sylib 
 |-  ( ( ph /\ y C_ J ) -> U. y C_ X )
11 vuniex 
 |-  U. y e. _V
12 11 elpw 
 |-  ( U. y e. ~P X <-> U. y C_ X )
13 10 12 sylibr 
 |-  ( ( ph /\ y C_ J ) -> U. y e. ~P X )
14 eluni2 
 |-  ( x e. U. y <-> E. z e. y x e. z )
15 elssuni 
 |-  ( z e. y -> z C_ U. y )
16 15 ad2antrl 
 |-  ( ( ( ph /\ y C_ J ) /\ ( z e. y /\ x e. z ) ) -> z C_ U. y )
17 16 sspwd 
 |-  ( ( ( ph /\ y C_ J ) /\ ( z e. y /\ x e. z ) ) -> ~P z C_ ~P U. y )
18 sslin 
 |-  ( ~P z C_ ~P U. y -> ( ( F ` x ) i^i ~P z ) C_ ( ( F ` x ) i^i ~P U. y ) )
19 17 18 syl 
 |-  ( ( ( ph /\ y C_ J ) /\ ( z e. y /\ x e. z ) ) -> ( ( F ` x ) i^i ~P z ) C_ ( ( F ` x ) i^i ~P U. y ) )
20 5 sselda 
 |-  ( ( ( ph /\ y C_ J ) /\ z e. y ) -> z e. J )
21 20 adantrr 
 |-  ( ( ( ph /\ y C_ J ) /\ ( z e. y /\ x e. z ) ) -> z e. J )
22 pweq 
 |-  ( o = z -> ~P o = ~P z )
23 22 ineq2d 
 |-  ( o = z -> ( ( F ` x ) i^i ~P o ) = ( ( F ` x ) i^i ~P z ) )
24 23 neeq1d 
 |-  ( o = z -> ( ( ( F ` x ) i^i ~P o ) =/= (/) <-> ( ( F ` x ) i^i ~P z ) =/= (/) ) )
25 24 raleqbi1dv 
 |-  ( o = z -> ( A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) <-> A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) )
26 25 4 elrab2 
 |-  ( z e. J <-> ( z e. ~P X /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) )
27 26 simprbi 
 |-  ( z e. J -> A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) )
28 21 27 syl 
 |-  ( ( ( ph /\ y C_ J ) /\ ( z e. y /\ x e. z ) ) -> A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) )
29 simprr 
 |-  ( ( ( ph /\ y C_ J ) /\ ( z e. y /\ x e. z ) ) -> x e. z )
30 rsp 
 |-  ( A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) -> ( x e. z -> ( ( F ` x ) i^i ~P z ) =/= (/) ) )
31 28 29 30 sylc 
 |-  ( ( ( ph /\ y C_ J ) /\ ( z e. y /\ x e. z ) ) -> ( ( F ` x ) i^i ~P z ) =/= (/) )
32 ssn0 
 |-  ( ( ( ( F ` x ) i^i ~P z ) C_ ( ( F ` x ) i^i ~P U. y ) /\ ( ( F ` x ) i^i ~P z ) =/= (/) ) -> ( ( F ` x ) i^i ~P U. y ) =/= (/) )
33 19 31 32 syl2anc 
 |-  ( ( ( ph /\ y C_ J ) /\ ( z e. y /\ x e. z ) ) -> ( ( F ` x ) i^i ~P U. y ) =/= (/) )
34 33 rexlimdvaa 
 |-  ( ( ph /\ y C_ J ) -> ( E. z e. y x e. z -> ( ( F ` x ) i^i ~P U. y ) =/= (/) ) )
35 14 34 syl5bi 
 |-  ( ( ph /\ y C_ J ) -> ( x e. U. y -> ( ( F ` x ) i^i ~P U. y ) =/= (/) ) )
36 35 ralrimiv 
 |-  ( ( ph /\ y C_ J ) -> A. x e. U. y ( ( F ` x ) i^i ~P U. y ) =/= (/) )
37 pweq 
 |-  ( o = U. y -> ~P o = ~P U. y )
38 37 ineq2d 
 |-  ( o = U. y -> ( ( F ` x ) i^i ~P o ) = ( ( F ` x ) i^i ~P U. y ) )
39 38 neeq1d 
 |-  ( o = U. y -> ( ( ( F ` x ) i^i ~P o ) =/= (/) <-> ( ( F ` x ) i^i ~P U. y ) =/= (/) ) )
40 39 raleqbi1dv 
 |-  ( o = U. y -> ( A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) <-> A. x e. U. y ( ( F ` x ) i^i ~P U. y ) =/= (/) ) )
41 40 4 elrab2 
 |-  ( U. y e. J <-> ( U. y e. ~P X /\ A. x e. U. y ( ( F ` x ) i^i ~P U. y ) =/= (/) ) )
42 13 36 41 sylanbrc 
 |-  ( ( ph /\ y C_ J ) -> U. y e. J )
43 42 ex 
 |-  ( ph -> ( y C_ J -> U. y e. J ) )
44 43 alrimiv 
 |-  ( ph -> A. y ( y C_ J -> U. y e. J ) )
45 pweq 
 |-  ( o = y -> ~P o = ~P y )
46 45 ineq2d 
 |-  ( o = y -> ( ( F ` x ) i^i ~P o ) = ( ( F ` x ) i^i ~P y ) )
47 46 neeq1d 
 |-  ( o = y -> ( ( ( F ` x ) i^i ~P o ) =/= (/) <-> ( ( F ` x ) i^i ~P y ) =/= (/) ) )
48 47 raleqbi1dv 
 |-  ( o = y -> ( A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) <-> A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) ) )
49 48 4 elrab2 
 |-  ( y e. J <-> ( y e. ~P X /\ A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) ) )
50 49 26 anbi12i 
 |-  ( ( y e. J /\ z e. J ) <-> ( ( y e. ~P X /\ A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) ) /\ ( z e. ~P X /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) ) )
51 an4 
 |-  ( ( ( y e. ~P X /\ A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) ) /\ ( z e. ~P X /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) ) <-> ( ( y e. ~P X /\ z e. ~P X ) /\ ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) ) )
52 50 51 bitri 
 |-  ( ( y e. J /\ z e. J ) <-> ( ( y e. ~P X /\ z e. ~P X ) /\ ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) ) )
53 inss1 
 |-  ( y i^i z ) C_ y
54 elpwi 
 |-  ( y e. ~P X -> y C_ X )
55 53 54 sstrid 
 |-  ( y e. ~P X -> ( y i^i z ) C_ X )
56 55 ad2antrl 
 |-  ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) -> ( y i^i z ) C_ X )
57 56 adantrr 
 |-  ( ( ph /\ ( ( y e. ~P X /\ z e. ~P X ) /\ ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) ) ) -> ( y i^i z ) C_ X )
58 vex 
 |-  y e. _V
59 58 inex1 
 |-  ( y i^i z ) e. _V
60 59 elpw 
 |-  ( ( y i^i z ) e. ~P X <-> ( y i^i z ) C_ X )
61 57 60 sylibr 
 |-  ( ( ph /\ ( ( y e. ~P X /\ z e. ~P X ) /\ ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) ) ) -> ( y i^i z ) e. ~P X )
62 ssralv 
 |-  ( ( y i^i z ) C_ y -> ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) -> A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P y ) =/= (/) ) )
63 53 62 ax-mp 
 |-  ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) -> A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P y ) =/= (/) )
64 inss2 
 |-  ( y i^i z ) C_ z
65 ssralv 
 |-  ( ( y i^i z ) C_ z -> ( A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) -> A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P z ) =/= (/) ) )
66 64 65 ax-mp 
 |-  ( A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) -> A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P z ) =/= (/) )
67 63 66 anim12i 
 |-  ( ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) -> ( A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P y ) =/= (/) /\ A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P z ) =/= (/) ) )
68 r19.26 
 |-  ( A. x e. ( y i^i z ) ( ( ( F ` x ) i^i ~P y ) =/= (/) /\ ( ( F ` x ) i^i ~P z ) =/= (/) ) <-> ( A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P y ) =/= (/) /\ A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P z ) =/= (/) ) )
69 67 68 sylibr 
 |-  ( ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) -> A. x e. ( y i^i z ) ( ( ( F ` x ) i^i ~P y ) =/= (/) /\ ( ( F ` x ) i^i ~P z ) =/= (/) ) )
70 n0 
 |-  ( ( ( F ` x ) i^i ~P y ) =/= (/) <-> E. v v e. ( ( F ` x ) i^i ~P y ) )
71 n0 
 |-  ( ( ( F ` x ) i^i ~P z ) =/= (/) <-> E. w w e. ( ( F ` x ) i^i ~P z ) )
72 70 71 anbi12i 
 |-  ( ( ( ( F ` x ) i^i ~P y ) =/= (/) /\ ( ( F ` x ) i^i ~P z ) =/= (/) ) <-> ( E. v v e. ( ( F ` x ) i^i ~P y ) /\ E. w w e. ( ( F ` x ) i^i ~P z ) ) )
73 exdistrv 
 |-  ( E. v E. w ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) <-> ( E. v v e. ( ( F ` x ) i^i ~P y ) /\ E. w w e. ( ( F ` x ) i^i ~P z ) ) )
74 inss2 
 |-  ( ( F ` x ) i^i ~P y ) C_ ~P y
75 simprl 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> v e. ( ( F ` x ) i^i ~P y ) )
76 74 75 sseldi 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> v e. ~P y )
77 76 elpwid 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> v C_ y )
78 inss2 
 |-  ( ( F ` x ) i^i ~P z ) C_ ~P z
79 simprr 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> w e. ( ( F ` x ) i^i ~P z ) )
80 78 79 sseldi 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> w e. ~P z )
81 80 elpwid 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> w C_ z )
82 ss2in 
 |-  ( ( v C_ y /\ w C_ z ) -> ( v i^i w ) C_ ( y i^i z ) )
83 77 81 82 syl2anc 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> ( v i^i w ) C_ ( y i^i z ) )
84 83 sspwd 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> ~P ( v i^i w ) C_ ~P ( y i^i z ) )
85 sslin 
 |-  ( ~P ( v i^i w ) C_ ~P ( y i^i z ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) C_ ( ( F ` x ) i^i ~P ( y i^i z ) ) )
86 84 85 syl 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) C_ ( ( F ` x ) i^i ~P ( y i^i z ) ) )
87 simplll 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> ph )
88 56 ad2antrr 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> ( y i^i z ) C_ X )
89 simplr 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> x e. ( y i^i z ) )
90 88 89 sseldd 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> x e. X )
91 inss1 
 |-  ( ( F ` x ) i^i ~P y ) C_ ( F ` x )
92 91 75 sseldi 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> v e. ( F ` x ) )
93 inss1 
 |-  ( ( F ` x ) i^i ~P z ) C_ ( F ` x )
94 93 79 sseldi 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> w e. ( F ` x ) )
95 87 90 92 94 3 syl13anc 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) )
96 ssn0 
 |-  ( ( ( ( F ` x ) i^i ~P ( v i^i w ) ) C_ ( ( F ` x ) i^i ~P ( y i^i z ) ) /\ ( ( F ` x ) i^i ~P ( v i^i w ) ) =/= (/) ) -> ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) )
97 86 95 96 syl2anc 
 |-  ( ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) /\ ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) ) -> ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) )
98 97 ex 
 |-  ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) -> ( ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) -> ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) ) )
99 98 exlimdvv 
 |-  ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) -> ( E. v E. w ( v e. ( ( F ` x ) i^i ~P y ) /\ w e. ( ( F ` x ) i^i ~P z ) ) -> ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) ) )
100 73 99 syl5bir 
 |-  ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) -> ( ( E. v v e. ( ( F ` x ) i^i ~P y ) /\ E. w w e. ( ( F ` x ) i^i ~P z ) ) -> ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) ) )
101 72 100 syl5bi 
 |-  ( ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) /\ x e. ( y i^i z ) ) -> ( ( ( ( F ` x ) i^i ~P y ) =/= (/) /\ ( ( F ` x ) i^i ~P z ) =/= (/) ) -> ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) ) )
102 101 ralimdva 
 |-  ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) -> ( A. x e. ( y i^i z ) ( ( ( F ` x ) i^i ~P y ) =/= (/) /\ ( ( F ` x ) i^i ~P z ) =/= (/) ) -> A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) ) )
103 69 102 syl5 
 |-  ( ( ph /\ ( y e. ~P X /\ z e. ~P X ) ) -> ( ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) -> A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) ) )
104 103 impr 
 |-  ( ( ph /\ ( ( y e. ~P X /\ z e. ~P X ) /\ ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) ) ) -> A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) )
105 pweq 
 |-  ( o = ( y i^i z ) -> ~P o = ~P ( y i^i z ) )
106 105 ineq2d 
 |-  ( o = ( y i^i z ) -> ( ( F ` x ) i^i ~P o ) = ( ( F ` x ) i^i ~P ( y i^i z ) ) )
107 106 neeq1d 
 |-  ( o = ( y i^i z ) -> ( ( ( F ` x ) i^i ~P o ) =/= (/) <-> ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) ) )
108 107 raleqbi1dv 
 |-  ( o = ( y i^i z ) -> ( A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) <-> A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) ) )
109 108 4 elrab2 
 |-  ( ( y i^i z ) e. J <-> ( ( y i^i z ) e. ~P X /\ A. x e. ( y i^i z ) ( ( F ` x ) i^i ~P ( y i^i z ) ) =/= (/) ) )
110 61 104 109 sylanbrc 
 |-  ( ( ph /\ ( ( y e. ~P X /\ z e. ~P X ) /\ ( A. x e. y ( ( F ` x ) i^i ~P y ) =/= (/) /\ A. x e. z ( ( F ` x ) i^i ~P z ) =/= (/) ) ) ) -> ( y i^i z ) e. J )
111 52 110 sylan2b 
 |-  ( ( ph /\ ( y e. J /\ z e. J ) ) -> ( y i^i z ) e. J )
112 111 ralrimivva 
 |-  ( ph -> A. y e. J A. z e. J ( y i^i z ) e. J )
113 sspwuni 
 |-  ( J C_ ~P X <-> U. J C_ X )
114 7 113 mpbi 
 |-  U. J C_ X
115 114 a1i 
 |-  ( ph -> U. J C_ X )
116 1 115 ssexd 
 |-  ( ph -> U. J e. _V )
117 uniexb 
 |-  ( J e. _V <-> U. J e. _V )
118 116 117 sylibr 
 |-  ( ph -> J e. _V )
119 istopg 
 |-  ( J e. _V -> ( J e. Top <-> ( A. y ( y C_ J -> U. y e. J ) /\ A. y e. J A. z e. J ( y i^i z ) e. J ) ) )
120 118 119 syl 
 |-  ( ph -> ( J e. Top <-> ( A. y ( y C_ J -> U. y e. J ) /\ A. y e. J A. z e. J ( y i^i z ) e. J ) ) )
121 44 112 120 mpbir2and 
 |-  ( ph -> J e. Top )
122 pwidg 
 |-  ( X e. V -> X e. ~P X )
123 1 122 syl 
 |-  ( ph -> X e. ~P X )
124 2 ffvelrnda 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) e. ( ~P ~P X \ { (/) } ) )
125 eldifi 
 |-  ( ( F ` x ) e. ( ~P ~P X \ { (/) } ) -> ( F ` x ) e. ~P ~P X )
126 elpwi 
 |-  ( ( F ` x ) e. ~P ~P X -> ( F ` x ) C_ ~P X )
127 124 125 126 3syl 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) C_ ~P X )
128 df-ss 
 |-  ( ( F ` x ) C_ ~P X <-> ( ( F ` x ) i^i ~P X ) = ( F ` x ) )
129 127 128 sylib 
 |-  ( ( ph /\ x e. X ) -> ( ( F ` x ) i^i ~P X ) = ( F ` x ) )
130 eldifsni 
 |-  ( ( F ` x ) e. ( ~P ~P X \ { (/) } ) -> ( F ` x ) =/= (/) )
131 124 130 syl 
 |-  ( ( ph /\ x e. X ) -> ( F ` x ) =/= (/) )
132 129 131 eqnetrd 
 |-  ( ( ph /\ x e. X ) -> ( ( F ` x ) i^i ~P X ) =/= (/) )
133 132 ralrimiva 
 |-  ( ph -> A. x e. X ( ( F ` x ) i^i ~P X ) =/= (/) )
134 pweq 
 |-  ( o = X -> ~P o = ~P X )
135 134 ineq2d 
 |-  ( o = X -> ( ( F ` x ) i^i ~P o ) = ( ( F ` x ) i^i ~P X ) )
136 135 neeq1d 
 |-  ( o = X -> ( ( ( F ` x ) i^i ~P o ) =/= (/) <-> ( ( F ` x ) i^i ~P X ) =/= (/) ) )
137 136 raleqbi1dv 
 |-  ( o = X -> ( A. x e. o ( ( F ` x ) i^i ~P o ) =/= (/) <-> A. x e. X ( ( F ` x ) i^i ~P X ) =/= (/) ) )
138 137 4 elrab2 
 |-  ( X e. J <-> ( X e. ~P X /\ A. x e. X ( ( F ` x ) i^i ~P X ) =/= (/) ) )
139 123 133 138 sylanbrc 
 |-  ( ph -> X e. J )
140 elssuni 
 |-  ( X e. J -> X C_ U. J )
141 139 140 syl 
 |-  ( ph -> X C_ U. J )
142 141 115 eqssd 
 |-  ( ph -> X = U. J )
143 istopon 
 |-  ( J e. ( TopOn ` X ) <-> ( J e. Top /\ X = U. J ) )
144 121 142 143 sylanbrc 
 |-  ( ph -> J e. ( TopOn ` X ) )