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 simpr 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) )
63 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 ) )
64 62 63 sylib 
 |-  ( ( ( ( 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 ) )
65 64 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 ) )
66 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 ) ) )
67 65 66 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 ) ) )
68 64 simprd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w e. ( ~P ( ( r e. J |-> ( U. J \ r ) ) " y ) i^i Fin ) ) -> w e. Fin )
69 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 )
70 61 67 68 69 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 )
71 eqcom 
 |-  ( ( ( r e. y |-> ( U. J \ r ) ) " z ) = w <-> w = ( ( r e. y |-> ( U. J \ r ) ) " z ) )
72 71 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 ) )
73 70 72 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 ) )
74 simpr 
 |-  ( ( ( ( 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 inteqd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w = ( ( r e. y |-> ( U. J \ r ) ) " z ) ) -> |^| w = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
76 75 eqeq2d 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ w = ( ( r e. y |-> ( U. J \ r ) ) " z ) ) -> ( (/) = |^| w <-> (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) ) )
77 53 73 76 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 ) ) )
78 0ex 
 |-  (/) e. _V
79 imassrn 
 |-  ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ran ( r e. J |-> ( U. J \ r ) )
80 eqid 
 |-  ( r e. J |-> ( U. J \ r ) ) = ( r e. J |-> ( U. J \ r ) )
81 54 80 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 ) ) ) )
82 81 simpld 
 |-  ( J e. Top -> ( r e. J |-> ( U. J \ r ) ) : J -1-1-onto-> ( Clsd ` J ) )
83 f1ofo 
 |-  ( ( r e. J |-> ( U. J \ r ) ) : J -1-1-onto-> ( Clsd ` J ) -> ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) )
84 82 83 syl 
 |-  ( J e. Top -> ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) )
85 forn 
 |-  ( ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) -> ran ( r e. J |-> ( U. J \ r ) ) = ( Clsd ` J ) )
86 84 85 syl 
 |-  ( J e. Top -> ran ( r e. J |-> ( U. J \ r ) ) = ( Clsd ` J ) )
87 79 86 sseqtrid 
 |-  ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ( Clsd ` J ) )
88 fvex 
 |-  ( Clsd ` J ) e. _V
89 88 elpw2 
 |-  ( ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) <-> ( ( r e. J |-> ( U. J \ r ) ) " y ) C_ ( Clsd ` J ) )
90 87 89 sylibr 
 |-  ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
91 90 ad2antrr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
92 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 ) )
93 78 91 92 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 ) )
94 inundif 
 |-  ( ( ( ~P y i^i Fin ) i^i { (/) } ) u. ( ( ~P y i^i Fin ) \ { (/) } ) ) = ( ~P y i^i Fin )
95 94 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 )
96 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 ) )
97 95 96 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 ) )
98 elinel2 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z e. { (/) } )
99 elsni 
 |-  ( z e. { (/) } -> z = (/) )
100 98 99 syl 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> z = (/) )
101 100 unieqd 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = U. (/) )
102 uni0 
 |-  U. (/) = (/)
103 101 102 eqtrdi 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> U. z = (/) )
104 103 eqeq2d 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> ( U. J = U. z <-> U. J = (/) ) )
105 104 biimpd 
 |-  ( z e. ( ( ~P y i^i Fin ) i^i { (/) } ) -> ( U. J = U. z -> U. J = (/) ) )
106 105 rexlimiv 
 |-  ( E. z e. ( ( ~P y i^i Fin ) i^i { (/) } ) U. J = U. z -> U. J = (/) )
107 ssidd 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y C_ y )
108 simprr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = (/) )
109 0ss 
 |-  (/) C_ U. y
110 108 109 eqsstrdi 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J C_ U. y )
111 24 ad2antlr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y C_ U. J )
112 110 111 eqssd 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. J = U. y )
113 112 108 eqtr3d 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y = (/) )
114 113 3 eqeltrdi 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> U. y e. Fin )
115 pwfi 
 |-  ( U. y e. Fin <-> ~P U. y e. Fin )
116 114 115 sylib 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> ~P U. y e. Fin )
117 pwuni 
 |-  y C_ ~P U. y
118 ssfi 
 |-  ( ( ~P U. y e. Fin /\ y C_ ~P U. y ) -> y e. Fin )
119 116 117 118 sylancl 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. Fin )
120 elfpw 
 |-  ( y e. ( ~P y i^i Fin ) <-> ( y C_ y /\ y e. Fin ) )
121 107 119 120 sylanbrc 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. ( ~P y i^i Fin ) )
122 simprl 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y =/= (/) )
123 eldifsn 
 |-  ( y e. ( ( ~P y i^i Fin ) \ { (/) } ) <-> ( y e. ( ~P y i^i Fin ) /\ y =/= (/) ) )
124 121 122 123 sylanbrc 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> y e. ( ( ~P y i^i Fin ) \ { (/) } ) )
125 unieq 
 |-  ( z = y -> U. z = U. y )
126 125 rspceeqv 
 |-  ( ( y e. ( ( ~P y i^i Fin ) \ { (/) } ) /\ U. J = U. y ) -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z )
127 124 112 126 syl2anc 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ ( y =/= (/) /\ U. J = (/) ) ) -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z )
128 127 expr 
 |-  ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) -> ( U. J = (/) -> E. z e. ( ( ~P y i^i Fin ) \ { (/) } ) U. J = U. z ) )
129 106 128 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 ) )
130 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 ) )
131 129 130 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 ) )
132 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 ) )
133 131 132 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 ) )
134 97 133 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 ) )
135 eldifi 
 |-  ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) -> z e. ( ~P y i^i Fin ) )
136 135 adantl 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z e. ( ~P y i^i Fin ) )
137 elfpw 
 |-  ( z e. ( ~P y i^i Fin ) <-> ( z C_ y /\ z e. Fin ) )
138 136 137 sylib 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( z C_ y /\ z e. Fin ) )
139 138 simpld 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ y )
140 simpllr 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> y C_ J )
141 139 140 sstrd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z C_ J )
142 141 unissd 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> U. z C_ U. J )
143 eqss 
 |-  ( U. z = U. J <-> ( U. z C_ U. J /\ U. J C_ U. z ) )
144 143 baib 
 |-  ( U. z C_ U. J -> ( U. z = U. J <-> U. J C_ U. z ) )
145 142 144 syl 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( U. z = U. J <-> U. J C_ U. z ) )
146 eqcom 
 |-  ( U. z = U. J <-> U. J = U. z )
147 ssdif0 
 |-  ( U. J C_ U. z <-> ( U. J \ U. z ) = (/) )
148 eqcom 
 |-  ( ( U. J \ U. z ) = (/) <-> (/) = ( U. J \ U. z ) )
149 147 148 bitri 
 |-  ( U. J C_ U. z <-> (/) = ( U. J \ U. z ) )
150 145 146 149 3bitr3g 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> ( U. J = U. z <-> (/) = ( U. J \ U. z ) ) )
151 df-ima 
 |-  ( ( r e. y |-> ( U. J \ r ) ) " z ) = ran ( ( r e. y |-> ( U. J \ r ) ) |` z )
152 139 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 ) ) )
153 152 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 ) ) )
154 151 153 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 ) ) )
155 154 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 ) ) )
156 56 ralrimivw 
 |-  ( J e. Top -> A. r e. z ( U. J \ r ) e. _V )
157 156 ad3antrrr 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> A. r e. z ( U. J \ r ) e. _V )
158 dfiin3g 
 |-  ( A. r e. z ( U. J \ r ) e. _V -> |^|_ r e. z ( U. J \ r ) = |^| ran ( r e. z |-> ( U. J \ r ) ) )
159 157 158 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 ) ) )
160 eldifsni 
 |-  ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) -> z =/= (/) )
161 160 adantl 
 |-  ( ( ( ( J e. Top /\ y C_ J ) /\ y =/= (/) ) /\ z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) -> z =/= (/) )
162 iindif2 
 |-  ( z =/= (/) -> |^|_ r e. z ( U. J \ r ) = ( U. J \ U_ r e. z r ) )
163 161 162 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 ) )
164 155 159 163 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 ) )
165 uniiun 
 |-  U. z = U_ r e. z r
166 165 difeq2i 
 |-  ( U. J \ U. z ) = ( U. J \ U_ r e. z r )
167 164 166 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 ) )
168 167 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 ) ) )
169 150 168 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 ) ) )
170 169 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 ) ) )
171 134 170 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 ) ) )
172 imaeq2 
 |-  ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = ( ( r e. y |-> ( U. J \ r ) ) " (/) ) )
173 ima0 
 |-  ( ( r e. y |-> ( U. J \ r ) ) " (/) ) = (/)
174 172 173 eqtrdi 
 |-  ( z = (/) -> ( ( r e. y |-> ( U. J \ r ) ) " z ) = (/) )
175 174 inteqd 
 |-  ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = |^| (/) )
176 int0 
 |-  |^| (/) = _V
177 175 176 eqtrdi 
 |-  ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) = _V )
178 177 neeq1d 
 |-  ( z = (/) -> ( |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) =/= (/) <-> _V =/= (/) ) )
179 14 178 mpbiri 
 |-  ( z = (/) -> |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) =/= (/) )
180 179 necomd 
 |-  ( z = (/) -> (/) =/= |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) )
181 180 necon2i 
 |-  ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) -> z =/= (/) )
182 eldifsn 
 |-  ( z e. ( ( ~P y i^i Fin ) \ { (/) } ) <-> ( z e. ( ~P y i^i Fin ) /\ z =/= (/) ) )
183 182 rbaibr 
 |-  ( z =/= (/) -> ( z e. ( ~P y i^i Fin ) <-> z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) )
184 181 183 syl 
 |-  ( (/) = |^| ( ( r e. y |-> ( U. J \ r ) ) " z ) -> ( z e. ( ~P y i^i Fin ) <-> z e. ( ( ~P y i^i Fin ) \ { (/) } ) ) )
185 184 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 ) ) )
186 185 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 ) )
187 171 186 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 ) ) )
188 77 93 187 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 ) ) ) )
189 38 188 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 ) ) ) ) )
190 23 189 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 ) ) ) ) )
191 57 adantr 
 |-  ( ( J e. Top /\ y C_ J ) -> A. r e. y ( U. J \ r ) e. _V )
192 dfiin3g 
 |-  ( A. r e. y ( U. J \ r ) e. _V -> |^|_ r e. y ( U. J \ r ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
193 191 192 syl 
 |-  ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
194 44 inteqd 
 |-  ( ( J e. Top /\ y C_ J ) -> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = |^| ran ( r e. y |-> ( U. J \ r ) ) )
195 193 194 eqtr4d 
 |-  ( ( J e. Top /\ y C_ J ) -> |^|_ r e. y ( U. J \ r ) = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
196 195 eqeq1d 
 |-  ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) ) )
197 nne 
 |-  ( -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) = (/) )
198 196 197 bitr4di 
 |-  ( ( J e. Top /\ y C_ J ) -> ( |^|_ r e. y ( U. J \ r ) = (/) <-> -. |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
199 198 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 ) ) ) ) )
200 190 199 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 ) ) ) ) )
201 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 ) =/= (/) ) )
202 200 201 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 ) =/= (/) ) ) )
203 1 202 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 ) =/= (/) ) ) )
204 203 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 ) =/= (/) ) ) )
205 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 ) ) )
206 205 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 ) ) )
207 90 adantr 
 |-  ( ( J e. Top /\ y e. ~P J ) -> ( ( r e. J |-> ( U. J \ r ) ) " y ) e. ~P ( Clsd ` J ) )
208 simpl 
 |-  ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> J e. Top )
209 funmpt 
 |-  Fun ( r e. J |-> ( U. J \ r ) )
210 209 a1i 
 |-  ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> Fun ( r e. J |-> ( U. J \ r ) ) )
211 elpwi 
 |-  ( x e. ~P ( Clsd ` J ) -> x C_ ( Clsd ` J ) )
212 foima 
 |-  ( ( r e. J |-> ( U. J \ r ) ) : J -onto-> ( Clsd ` J ) -> ( ( r e. J |-> ( U. J \ r ) ) " J ) = ( Clsd ` J ) )
213 84 212 syl 
 |-  ( J e. Top -> ( ( r e. J |-> ( U. J \ r ) ) " J ) = ( Clsd ` J ) )
214 213 sseq2d 
 |-  ( J e. Top -> ( x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) <-> x C_ ( Clsd ` J ) ) )
215 211 214 imbitrrid 
 |-  ( J e. Top -> ( x e. ~P ( Clsd ` J ) -> x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) ) )
216 215 imp 
 |-  ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> x C_ ( ( r e. J |-> ( U. J \ r ) ) " J ) )
217 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 ) ) )
218 208 210 216 217 syl3anc 
 |-  ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> E. y ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
219 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 ) ) )
220 velpw 
 |-  ( y e. ~P J <-> y C_ J )
221 220 anbi1i 
 |-  ( ( y e. ~P J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) <-> ( y C_ J /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
222 221 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 ) ) )
223 219 222 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 ) ) )
224 218 223 sylibr 
 |-  ( ( J e. Top /\ x e. ~P ( Clsd ` J ) ) -> E. y e. ~P J x = ( ( r e. J |-> ( U. J \ r ) ) " y ) )
225 simpr 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> x = ( ( r e. J |-> ( U. J \ r ) ) " y ) )
226 225 fveq2d 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( fi ` x ) = ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) )
227 226 eleq2d 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( (/) e. ( fi ` x ) <-> (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
228 227 notbid 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( -. (/) e. ( fi ` x ) <-> -. (/) e. ( fi ` ( ( r e. J |-> ( U. J \ r ) ) " y ) ) ) )
229 225 inteqd 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> |^| x = |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) )
230 229 neeq1d 
 |-  ( ( J e. Top /\ x = ( ( r e. J |-> ( U. J \ r ) ) " y ) ) -> ( |^| x =/= (/) <-> |^| ( ( r e. J |-> ( U. J \ r ) ) " y ) =/= (/) ) )
231 228 230 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 ) =/= (/) ) ) )
232 207 224 231 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 ) =/= (/) ) ) )
233 204 206 232 3bitr4d 
 |-  ( J e. Top -> ( J e. Comp <-> A. x e. ~P ( Clsd ` J ) ( -. (/) e. ( fi ` x ) -> |^| x =/= (/) ) ) )