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

Metamath Proof Explorer

Theorem cmpfi

Description: If a topology is compact and a collection of closed sets has the finite intersection property, its intersection is nonempty. (Contributed by Jeff Hankins, 25-Aug-2009) (Proof shortened by Mario Carneiro, 1-Sep-2015)

Ref Expression
Assertion cmpfi 
|- ( J e. Top -> ( J e. Comp <-> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )

Proof

Step Hyp Ref Expression
1 elpwi 
 |-  ( y e. ~P J -> y C_ J )
2 0ss 
 |-  (/) C_ y
3 0fi 
 |-  (/) e. Fin
4 elfpw 
 |-  ( (/) e. ( ~P y i^i Fin ) <-> ( (/) C_ y /\ (/) e. Fin ) )
5 2 3 4 mpbir2an 
 |-  (/) e. ( ~P y i^i Fin )
6 simprr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. J = U. y )
7 simprl 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> y = (/) )
8 7 unieqd 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. y = U. (/) )
9 6 8 eqtrd 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> U. J = U. (/) )
10 unieq 
 |-  ( z = (/) -> U. z = U. (/) )
11 10 rspceeqv 
 |-  ( ( (/) e. ( ~P y i^i Fin ) /\ U. J = U. (/) ) -> E. z e. ( ~P y i^i Fin ) U. J = U. z )
12 5 9 11 sylancr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y = (/) /\ U. J = U. y ) ) -> E. z e. ( ~P y i^i Fin ) U. J = U. z )
13 12 expr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) )
14 vn0 
 |-  _V =/= (/)
15 iineq1 
 |-  ( y = (/) -> |^|_ r e. y ( U. J \ r ) = |^|_ r e. (/) ( U. J \ r ) )
16 15 adantl 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> |^|_ r e. y ( U. J \ r ) = |^|_ r e. (/) ( U. J \ r ) )
17 0iin 
 |-  |^|_ r e. (/) ( U. J \ r ) = _V
18 16 17 eqtrdi 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> |^|_ r e. y ( U. J \ r ) = _V )
19 18 eqeq1d 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> _V = (/) ) )
20 19 necon3bbid 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( -. |^|_ r e. y ( U. J \ r ) = (/) <-> _V =/= (/) ) )
21 14 20 mpbiri 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> -. |^|_ r e. y ( U. J \ r ) = (/) )
22 21 pm2.21d 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( |^|_ r e. y ( U. J \ r ) = (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
23 13 22 2thd 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y = (/) ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( |^|_ r e. y ( U. J \ r ) = (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) ) )
24 uniss 
 |-  ( y C_ J -> U. y C_ U. J )
25 24 ad2antlr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> U. y C_ U. J )
26 eqss 
 |-  ( U. y = U. J <-> ( U. y C_ U. J /\ U. J C_ U. y ) )
27 26 baib 
 |-  ( U. y C_ U. J -> ( U. y = U. J <-> U. J C_ U. y ) )
28 25 27 syl 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. y = U. J <-> U. J C_ U. y ) )
29 eqcom 
 |-  ( U. y = U. J <-> U. J = U. y )
30 ssdif0 
 |-  ( U. J C_ U. y <-> ( U. J \ U. y ) = (/) )
31 28 29 30 3bitr3g 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. J = U. y <-> ( U. J \ U. y ) = (/) ) )
32 iindif2 
 |-  ( y =/= (/) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U_ r e. y r ) )
33 32 adantl 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U_ r e. y r ) )
34 uniiun 
 |-  U. y = U_ r e. y r
35 34 difeq2i 
 |-  ( U. J \ U. y ) = ( U. J \ U_ r e. y r )
36 33 35 eqtr4di 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> |^|_ r e. y ( U. J \ r ) = ( U. J \ U. y ) )
37 36 eqeq1d 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> ( U. J \ U. y ) = (/) ) )
38 31 37 bitr4d 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. J = U. y <-> |^|_ r e. y ( U. J \ r ) = (/) ) )
39 imassrn 
 |-  ( ( r e. y |-> ( U. J \ r ) ) " z ) C_ ran ( r e. y |-> ( U. J \ r ) )
40 df-ima 
 |-  ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( ( r e. J |-> ( U. J \ r ) ) |` y )
41 resmpt 
 |-  ( y C_ J -> ( ( r e. J |-> ( U. J \ r ) ) |` y ) = ( r e. y |-> ( U. J \ r ) ) )
42 41 adantl 
 |-  ( ( J e. Top /\ y C_ J ) -> ( ( r e. J |-> ( U. J \ r ) ) |` y ) = ( r e. y |-> ( U. J \ r ) ) )
43 42 rneqd 
 |-  ( ( J e. Top /\ y C_ J ) -> ran ( ( r e. J |-> ( U. J \ r ) ) |` y ) = ran ( r e. y |-> ( U. J \ r ) ) )
44 40 43 eqtrid 
 |-  ( ( J e. Top /\ y C_ J ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( r e. y |-> ( U. J \ r ) ) )
45 44 ad2antrr 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( r e. y |-> ( U. J \ r ) ) )
46 39 45 sseqtrrid 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) C_ ( ( r e. J |-> ( U. J \ r ) ) " y ) )
47 funmpt 
 |-  Fun ( r e. y |-> ( U. J \ r ) )
48 elinel2 
 |-  ( z e. ( ~P y i^i Fin ) -> z e. Fin )
49 48 adantl 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> z e. Fin )
50 imafi 
 |-  ( ( Fun ( r e. y |-> ( U. J \ r ) ) /\ z e. Fin ) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) e. Fin )
51 47 49 50 sylancr 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) e. Fin )
52 elfpw 
 |-  ( ( ( r e. y |-> ( U. J \ r ) ) " z ) e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) <-> ( ( ( r e. y |-> ( U. J \ r ) ) " z ) C_ ( ( r e. J |-> ( U. J \ r ) ) " y ) /\ ( ( r e. y |-> ( U. J \ r ) ) " z ) e. Fin ) )
53 46 51 52 sylanbrc 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ~P y i^i Fin ) ) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) )
54 eqid 
 |-  U. J = U. J
55 54 topopn 
 |-  ( J e. Top -> U. J e. J )
56 55 difexd 
 |-  ( J e. Top -> ( U. J \ r ) e. _V )
57 56 ralrimivw 
 |-  ( J e. Top -> A. r e. y ( U. J \ r ) e. _V )
58 eqid 
 |-  ( r e. y |-> ( U. J \ r ) ) = ( r e. y |-> ( U. J \ r ) )
59 58 fnmpt 
 |-  ( A. r e. y ( U. J \ r ) e. _V -> ( r e. y |-> ( U. J \ r ) ) Fn y )
60 57 59 syl 
 |-  ( J e. Top -> ( r e. y |-> ( U. J \ r ) ) Fn y )
61 60 ad3antrrr 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> ( r e. y |-> ( U. J \ r ) ) Fn y )
62 elfpw 
 |-  ( w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) <-> ( w C_ ( ( r e. J |-> ( U. J \ r ) ) " y ) /\ w e. Fin ) )
63 62 bilani 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> ( w C_ ( ( r e. J |-> ( U. J \ r ) ) " y ) /\ w e. Fin ) )
64 63 simpld 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> w C_ ( ( r e. J |-> ( U. J \ r ) ) " y ) )
65 44 ad2antrr 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) = ran ( r e. y |-> ( U. J \ r ) ) )
66 64 65 sseqtrd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> w C_ ran ( r e. y |-> ( U. J \ r ) ) )
67 63 simprd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> w e. Fin )
68 fipreima 
 |-  ( ( ( r e. y |-> ( U. J \ r ) ) Fn y /\ w C_ ran ( r e. y |-> ( U. J \ r ) ) /\ w e. Fin ) -> E. z e. ( ~P y i^i Fin ) ( ( r e. y |-> ( U. J \ r ) ) " z ) = w )
69 61 66 67 68 syl3anc 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> E. z e. ( ~P y i^i Fin ) ( ( r e. y |-> ( U. J \ r ) ) " z ) = w )
70 eqcom 
 |-  ( ( ( r e. y |-> ( U. J \ r ) ) " z ) = w <-> w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
71 70 rexbii 
 |-  ( E. z e. ( ~P y i^i Fin ) ( ( r e. y |-> ( U. J \ r ) ) " z ) = w <-> E. z e. ( ~P y i^i Fin ) w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
72 69 71 sylib 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> E. z e. ( ~P y i^i Fin ) w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
73 simpr 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w = ( ( r e. y |-> ( U. J \ r ) ) " z ) ) -> w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
74 73 inteqd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w = ( ( r e. y |-> ( U. J \ r ) ) " z ) ) -> |^| w = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
75 74 eqeq2d 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w = ( ( r e. y |-> ( U. J \ r ) ) " z ) ) -> ( (/) = |^| w <-> (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
76 53 72 75 rexxfrd 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) (/) = |^| w <-> E. z e. ( ~P y i^i Fin ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
77 0ex 
 |-  (/) e. _V
78 imassrn 
 |-  ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ran ( r e. J |-> ( U. J \ r ) )
79 eqid 
 |-  ( r e. J |-> ( U. J \ r ) ) = ( r e. J |-> ( U. J \ r ) )
80 54 79 opncldf1 
 |-  ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) : J -1-1-onto-> ( Clsd ` J ) /\ `' ( r e. J |-> ( U. J \ r ) ) = ( v e. ( Clsd ` J ) |-> ( U. J \ v ) ) ) )
81 80 simpld 
 |-  ( J e. Top -> ( r e. J |-> ( U. J \ r ) ) : J -1-1-onto-> ( Clsd ` J ) )
82 f1ofo 
 |-  ( ( r e. J |-> ( U. J \ r ) ) : J -1-1-onto-> ( Clsd ` J ) -> ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) )
83 81 82 syl 
 |-  ( J e. Top -> ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) )
84 forn 
 |-  ( ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) -> ran ( r e. J |-> ( U. J \ r ) ) = ( Clsd ` J ) )
85 83 84 syl 
 |-  ( J e. Top -> ran ( r e. J |-> ( U. J \ r ) ) = ( Clsd ` J ) )
86 78 85 sseqtrid 
 |-  ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ( Clsd ` J ) )
87 fvex 
 |-  ( Clsd ` J ) e. _V
88 87 elpw2 
 |-  ( ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) <-> ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ( Clsd ` J ) )
89 86 88 sylibr 
 |-  ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
90 89 ad2antrr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
91 elfi 
 |-  ( ( (/) e. _V /\ ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) ) -> ( (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) <-> E. w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) (/) = |^| w ) )
92 77 90 91 sylancr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) <-> E. w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) (/) = |^| w ) )
93 inundif 
 |-  ( ( ( ~P y i^i Fin ) i^i { (/) } ) u. ( ( ~P y i^i Fin ) \ { (/) } ) ) = ( ~P y i^i Fin )
94 93 rexeqi 
 |-  ( E. z e. ( ( ( ~P y i^i Fin ) i^i { (/) } ) u. ( ( ~P y i^i Fin ) \ { (/) } ) ) U. J = U. z <-> E. z e. ( ~P y i^i Fin ) U. J = U. z )
95 rexun 
 |-  ( E. z e. ( ( ( ~P y i^i Fin ) i^i { (/) } ) u. ( ( ~P y i^i Fin ) \ { (/) } ) ) U. J = U. z <-> ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z \/ E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
96 94 95 bitr3i 
 |-  ( E. z e. ( ~P y i^i Fin ) U. J = U. z <-> ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z \/ E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
97 elinel2 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z e. { (/) } )
98 elsni 
 |-  ( z e. { (/) } -> z = (/) )
99 97 98 syl 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z = (/) )
100 99 unieqd 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = U. (/) )
101 uni0 
 |-  U. (/) = (/)
102 100 101 eqtrdi 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = (/) )
103 102 eqeq2d 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> ( U. J = U. z <-> U. J = (/) ) )
104 103 biimpd 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> ( U. J = U. z -> U. J = (/) ) )
105 104 rexlimiv 
 |-  ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z -> U. J = (/) )
106 ssidd 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y C_ y )
107 simprr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = (/) )
108 0ss 
 |-  (/) C_ U. y
109 107 108 eqsstrdi 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J C_ U. y )
110 24 ad2antlr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y C_ U. J )
111 109 110 eqssd 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = U. y )
112 111 107 eqtr3d 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y = (/) )
113 112 3 eqeltrdi 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y e. Fin )
114 pwfi 
 |-  ( U. y e. Fin <-> ~P U. y e. Fin )
115 113 114 sylib 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> ~P U. y e. Fin )
116 pwuni 
 |-  y C_ ~P U. y
117 ssfi 
 |-  ( ( ~P U. y e. Fin /\ y C_ ~P U. y ) -> y e. Fin )
118 115 116 117 sylancl 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. Fin )
119 elfpw 
 |-  ( y e. ( ~P y i^i Fin ) <-> ( y C_ y /\ y e. Fin ) )
120 106 118 119 sylanbrc 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. ( ~P y i^i Fin ) )
121 simprl 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y =/= (/) )
122 eldifsn 
 |-  ( y e. ( ( ~P y i^i Fin ) \ { (/) } ) <-> ( y e. ( ~P y i^i Fin ) /\ y =/= (/) ) )
123 120 121 122 sylanbrc 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. ( ( ~P y i^i Fin ) \ { (/) } ) )
124 unieq 
 |-  ( z = y -> U. z = U. y )
125 124 rspceeqv 
 |-  ( ( y e. ( ( ~P y i^i Fin ) \ { (/) } ) /\ U. J = U. y ) -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z )
126 123 111 125 syl2anc 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z )
127 126 expr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. J = (/) -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
128 105 127 syl5 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
129 idd 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
130 128 129 jaod 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z \/ E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
131 olc 
 |-  ( E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z -> ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z \/ E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
132 130 131 impbid1 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z \/ E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) <-> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
133 96 132 bitrid 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ~P y i^i Fin ) U. J = U. z <-> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
134 eldifi 
 |-  ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) -> z e. ( ~P y i^i Fin ) )
135 134 adantl 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z e. ( ~P y i^i Fin ) )
136 elfpw 
 |-  ( z e. ( ~P y i^i Fin ) <-> ( z C_ y /\ z e. Fin ) )
137 135 136 sylib 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( z C_ y /\ z e. Fin ) )
138 137 simpld 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ y )
139 simpllr 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> y C_ J )
140 138 139 sstrd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ J )
141 140 unissd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> U. z C_ U. J )
142 eqss 
 |-  ( U. z = U. J <-> ( U. z C_ U. J /\ U. J C_ U. z ) )
143 142 baib 
 |-  ( U. z C_ U. J -> ( U. z = U. J <-> U. J C_ U. z ) )
144 141 143 syl 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( U. z = U. J <-> U. J C_ U. z ) )
145 eqcom 
 |-  ( U. z = U. J <-> U. J = U. z )
146 ssdif0 
 |-  ( U. J C_ U. z <-> ( U. J \ U. z ) = (/) )
147 eqcom 
 |-  ( ( U. J \ U. z ) = (/) <-> (/) = ( U. J \ U. z ) )
148 146 147 bitri 
 |-  ( U. J C_ U. z <-> (/) = ( U. J \ U. z ) )
149 144 145 148 3bitr3g 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( U. J = U. z <-> (/) = ( U. J \ U. z ) ) )
150 df-ima 
 |-  ( ( r e. y |-> ( U. J \ r ) ) " z ) = ran ( ( r e. y |-> ( U. J \ r ) ) |` z )
151 138 resmptd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( ( r e. y |-> ( U. J \ r ) ) |` z ) = ( r e. z |-> ( U. J \ r ) ) )
152 151 rneqd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ran ( ( r e. y |-> ( U. J \ r ) ) |` z ) = ran ( r e. z |-> ( U. J \ r ) ) )
153 150 152 eqtrid 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = ran ( r e. z |-> ( U. J \ r ) ) )
154 153 inteqd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = |^| ran ( r e. z |-> ( U. J \ r ) ) )
155 56 ralrimivw 
 |-  ( J e. Top -> A. r e. z ( U. J \ r ) e. _V )
156 155 ad3antrrr 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> A. r e. z ( U. J \ r ) e. _V )
157 dfiin3g 
 |-  ( A. r e. z ( U. J \ r ) e. _V -> |^|_ r e. z ( U. J \ r ) = |^| ran ( r e. z |-> ( U. J \ r ) ) )
158 156 157 syl 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> |^|_ r e. z ( U. J \ r ) = |^| ran ( r e. z |-> ( U. J \ r ) ) )
159 eldifsni 
 |-  ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) -> z =/= (/) )
160 159 adantl 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z =/= (/) )
161 iindif2 
 |-  ( z =/= (/) -> |^|_ r e. z ( U. J \ r ) = ( U. J \ U_ r e. z r ) )
162 160 161 syl 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> |^|_ r e. z ( U. J \ r ) = ( U. J \ U_ r e. z r ) )
163 154 158 162 3eqtr2d 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = ( U. J \ U_ r e. z r ) )
164 uniiun 
 |-  U. z = U_ r e. z r
165 164 difeq2i 
 |-  ( U. J \ U. z ) = ( U. J \ U_ r e. z r )
166 163 165 eqtr4di 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = ( U. J \ U. z ) )
167 166 eqeq2d 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) <-> (/) = ( U. J \ U. z ) ) )
168 149 167 bitr4d 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( U. J = U. z <-> (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
169 168 rexbidva 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z <-> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
170 133 169 bitrd 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ~P y i^i Fin ) U. J = U. z <-> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
171 imaeq2 
 |-  ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = ( ( r e. y |-> ( U. J \ r ) ) " (/) ) )
172 ima0 
 |-  ( ( r e. y |-> ( U. J \ r ) ) " (/) ) = (/)
173 171 172 eqtrdi 
 |-  ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = (/) )
174 173 inteqd 
 |-  ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = |^| (/) )
175 int0 
 |-  |^| (/) = _V
176 174 175 eqtrdi 
 |-  ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = _V )
177 176 neeq1d 
 |-  ( z = (/) -> ( |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) =/= (/) <-> _V =/= (/) ) )
178 14 177 mpbiri 
 |-  ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) =/= (/) )
179 178 necomd 
 |-  ( z = (/) -> (/) =/= |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
180 179 necon2i 
 |-  ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) -> z =/= (/) )
181 eldifsn 
 |-  ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) <-> ( z e. ( ~P y i^i Fin ) /\ z =/= (/) ) )
182 181 rbaibr 
 |-  ( z =/= (/) -> ( z e. ( ~P y i^i Fin ) <-> z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) )
183 180 182 syl 
 |-  ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) -> ( z e. ( ~P y i^i Fin ) <-> z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) )
184 183 pm5.32ri 
 |-  ( ( z e. ( ~P y i^i Fin ) /\ (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) <-> ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) /\ (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
185 184 rexbii2 
 |-  ( E. z e. ( ~P y i^i Fin ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) <-> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
186 170 185 bitr4di 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ~P y i^i Fin ) U. J = U. z <-> E. z e. ( ~P y i^i Fin ) (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
187 76 92 186 3bitr4rd 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( E. z e. ( ~P y i^i Fin ) U. J = U. z <-> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
188 38 187 imbi12d 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( |^|_ r e. y ( U. J \ r ) = (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) ) )
189 23 188 pm2.61dane 
 |-  ( ( J e. Top /\ y C_ J ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( |^|_ r e. y ( U. J \ r ) = (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) ) )
190 57 adantr 
 |-  ( ( J e. Top /\ y C_ J ) -> A. r e. y ( U. J \ r ) e. _V )
191 dfiin3g 
 |-  ( A. r e. y ( U. J \ r ) e. _V -> |^|_ r e. y ( U. J \ r ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
192 190 191 syl 
 |-  ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
193 44 inteqd 
 |-  ( ( J e. Top /\ y C_ J ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
194 192 193 eqtr4d 
 |-  ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
195 194 eqeq1d 
 |-  ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) ) )
196 nne 
 |-  ( -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) )
197 195 196 bitr4di 
 |-  ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
198 197 imbi1d 
 |-  ( ( J e. Top /\ y C_ J ) -> ( ( |^|_ r e. y ( U. J \ r ) = (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) <-> ( -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) ) )
199 189 198 bitrd 
 |-  ( ( J e. Top /\ y C_ J ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) ) )
200 con1b 
 |-  ( ( -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) -> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) <-> ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
201 199 200 bitrdi 
 |-  ( ( J e. Top /\ y C_ J ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) ) )
202 1 201 sylan2 
 |-  ( ( J e. Top /\ y e. ~P J ) -> ( ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) ) )
203 202 ralbidva 
 |-  ( J e. Top -> ( A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) <-> A. y e. ~P J ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) ) )
204 54 iscmp 
 |-  ( J e. Comp <-> ( J e. Top /\ A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) )
205 204 baib 
 |-  ( J e. Top -> ( J e. Comp <-> A. y e. ~P J ( U. J = U. y -> E. z e. ( ~P y i^i Fin ) U. J = U. z ) ) )
206 89 adantr 
 |-  ( ( J e. Top /\ y e. ~P J ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
207 simpl 
 |-  ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> J e. Top )
208 funmpt 
 |-  Fun ( r e. J |-> ( U. J \ r ) )
209 208 a1i 
 |-  ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> Fun ( r e. J |-> ( U. J \ r ) ) )
210 elpwi 
 |-  ( x e. ~P ( Clsd ` J ) -> x C_ ( Clsd ` J ) )
211 foima 
 |-  ( ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) -> ( ( r e. J |-> ( U. J \ r ) ) " J ) = ( Clsd ` J ) )
212 83 211 syl 
 |-  ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " J ) = ( Clsd ` J ) )
213 212 sseq2d 
 |-  ( J e. Top -> ( x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) <-> x C_ ( Clsd ` J ) ) )
214 210 213 imbitrrid 
 |-  ( J e. Top -> ( x e. ~P ( Clsd ` J ) -> x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) ) )
215 214 imp 
 |-  ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) )
216 ssimaexg 
 |-  ( ( J e. Top /\ Fun ( r e. J |-> ( U. J \ r ) ) /\ x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) ) -> E. y ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
217 207 209 215 216 syl3anc 
 |-  ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> E. y ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
218 df-rex 
 |-  ( E. y e. ~P J x = ( ( r e. J |-> ( U. J \ r ) ) " y ) <-> E. y ( y e. ~P J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
219 velpw 
 |-  ( y e. ~P J <-> y C_ J )
220 219 anbi1i 
 |-  ( ( y e. ~P J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) <-> ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
221 220 exbii 
 |-  ( E. y ( y e. ~P J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) <-> E. y ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
222 218 221 bitri 
 |-  ( E. y e. ~P J x = ( ( r e. J |-> ( U. J \ r ) ) " y ) <-> E. y ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
223 217 222 sylibr 
 |-  ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> E. y e. ~P J x = ( ( r e. J |-> ( U. J \ r ) ) " y ) )
224 simpr 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> x = ( ( r e. J |-> ( U. J \ r ) ) " y ) )
225 224 fveq2d 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( fi ` x ) = ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
226 225 eleq2d 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( (/) e. ( fi ` x ) <-> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
227 226 notbid 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( -. (/) e. ( fi ` x ) <-> -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
228 224 inteqd 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| x = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
229 228 neeq1d 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( |^| x =/= (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
230 227 229 imbi12d 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) <-> ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) ) )
231 206 223 230 ralxfrd 
 |-  ( J e. Top -> ( A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) <-> A. y e. ~P J ( -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) ) )
232 203 205 231 3bitr4d 
 |-  ( J e. Top -> ( J e. Comp <-> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )