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 ( 𝐽 ∈ Top → ( 𝐽 ∈ Comp ↔ ∀ 𝑥 ∈ 𝒫 ( Clsd ‘ 𝐽 ) ( ¬ ∅ ∈ ( fi ‘ 𝑥 ) → 𝑥 ≠ ∅ ) ) )

Proof

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