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