Metamath Proof Explorer

Theorem cmpsub

Description: Two equivalent ways of describing a compact subset of a topological space. Inspired by Sue E. Goodman'sBeginning Topology. (Contributed by Jeff Hankins, 22-Jun-2009) (Revised by Mario Carneiro, 15-Dec-2013)

Ref Expression
Hypothesis cmpsub.1 ⊢ 𝑋 = ∪ 𝐽
Assertion cmpsub ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) )

Proof

Step Hyp Ref Expression
1 cmpsub.1 ⊢ 𝑋 = ∪ 𝐽
2 eqid ⊢ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ ( 𝐽 ↾t 𝑆 )
3 2 iscmp ⊢ ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ↔ ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
4 id ⊢ ( 𝑆 ⊆ 𝑋 → 𝑆 ⊆ 𝑋 )
5 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
6 ssexg ⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽 ) → 𝑆 ∈ V )
7 4 5 6 syl2anr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ V )
8 resttop ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝐽 ↾t 𝑆 ) ∈ Top )
9 7 8 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑆 ) ∈ Top )
10 ibar ⊢ ( ( 𝐽 ↾t 𝑆 ) ∈ Top → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ↔ ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ) )
11 10 bicomd ⊢ ( ( 𝐽 ↾t 𝑆 ) ∈ Top → ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
12 9 11 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( 𝐽 ↾t 𝑆 ) ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
13 3 12 bitrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ↔ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
14 vex ⊢ 𝑡 ∈ V
15 eqeq1 ⊢ ( 𝑥 = 𝑡 → ( 𝑥 = ( 𝑦 ∩ 𝑆 ) ↔ 𝑡 = ( 𝑦 ∩ 𝑆 ) ) )
16 15 rexbidv ⊢ ( 𝑥 = 𝑡 → ( ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) ↔ ∃ 𝑦 ∈ 𝑐 𝑡 = ( 𝑦 ∩ 𝑆 ) ) )
17 14 16 elab ⊢ ( 𝑡 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ ∃ 𝑦 ∈ 𝑐 𝑡 = ( 𝑦 ∩ 𝑆 ) )
18 velpw ⊢ ( 𝑐 ∈ 𝒫 𝐽 ↔ 𝑐 ⊆ 𝐽 )
19 ssel2 ⊢ ( ( 𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐 ) → 𝑦 ∈ 𝐽 )
20 ineq1 ⊢ ( 𝑑 = 𝑦 → ( 𝑑 ∩ 𝑆 ) = ( 𝑦 ∩ 𝑆 ) )
21 20 rspceeqv ⊢ ( ( 𝑦 ∈ 𝐽 ∧ 𝑡 = ( 𝑦 ∩ 𝑆 ) ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) )
22 21 ex ⊢ ( 𝑦 ∈ 𝐽 → ( 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) )
23 19 22 syl ⊢ ( ( 𝑐 ⊆ 𝐽 ∧ 𝑦 ∈ 𝑐 ) → ( 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) )
24 23 ex ⊢ ( 𝑐 ⊆ 𝐽 → ( 𝑦 ∈ 𝑐 → ( 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) ) )
25 18 24 sylbi ⊢ ( 𝑐 ∈ 𝒫 𝐽 → ( 𝑦 ∈ 𝑐 → ( 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) ) )
26 25 adantl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑦 ∈ 𝑐 → ( 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) ) )
27 26 rexlimdv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∃ 𝑦 ∈ 𝑐 𝑡 = ( 𝑦 ∩ 𝑆 ) → ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) )
28 simpll ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → 𝐽 ∈ Top )
29 1 sseq2i ⊢ ( 𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽 )
30 uniexg ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ V )
31 ssexg ⊢ ( ( 𝑆 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ∈ V ) → 𝑆 ∈ V )
32 30 31 sylan2 ⊢ ( ( 𝑆 ⊆ ∪ 𝐽 ∧ 𝐽 ∈ Top ) → 𝑆 ∈ V )
33 32 ancoms ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → 𝑆 ∈ V )
34 29 33 sylan2b ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ V )
35 34 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → 𝑆 ∈ V )
36 elrest ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝑡 ∈ ( 𝐽 ↾t 𝑆 ) ↔ ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) )
37 28 35 36 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑡 ∈ ( 𝐽 ↾t 𝑆 ) ↔ ∃ 𝑑 ∈ 𝐽 𝑡 = ( 𝑑 ∩ 𝑆 ) ) )
38 27 37 sylibrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∃ 𝑦 ∈ 𝑐 𝑡 = ( 𝑦 ∩ 𝑆 ) → 𝑡 ∈ ( 𝐽 ↾t 𝑆 ) ) )
39 17 38 biimtrid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑡 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → 𝑡 ∈ ( 𝐽 ↾t 𝑆 ) ) )
40 39 ssrdv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ⊆ ( 𝐽 ↾t 𝑆 ) )
41 vex ⊢ 𝑐 ∈ V
42 41 abrexex ⊢ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∈ V
43 42 elpw ⊢ ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ↔ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ⊆ ( 𝐽 ↾t 𝑆 ) )
44 40 43 sylibr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) )
45 unieq ⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∪ 𝑠 = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } )
46 45 eqeq2d ⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 ↔ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ) )
47 pweq ⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → 𝒫 𝑠 = 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } )
48 47 ineq1d ⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ( 𝒫 𝑠 ∩ Fin ) = ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) )
49 48 rexeqdv ⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ( ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ↔ ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) )
50 46 49 imbi12d ⊢ ( 𝑠 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ( ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ↔ ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
51 50 rspcva ⊢ ( ( { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) → ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) )
52 44 51 sylan ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) → ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) )
53 52 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
54 1 restuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) )
55 54 ad2antrr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) )
56 vex ⊢ 𝑦 ∈ V
57 56 inex1 ⊢ ( 𝑦 ∩ 𝑆 ) ∈ V
58 57 dfiun2 ⊢ ∪ 𝑦 ∈ 𝑐 ( 𝑦 ∩ 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) }
59 incom ⊢ ( 𝑦 ∩ 𝑆 ) = ( 𝑆 ∩ 𝑦 )
60 59 a1i ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ 𝑦 ∈ 𝑐 ) → ( 𝑦 ∩ 𝑆 ) = ( 𝑆 ∩ 𝑦 ) )
61 60 iuneq2dv ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ∪ 𝑦 ∈ 𝑐 ( 𝑦 ∩ 𝑆 ) = ∪ 𝑦 ∈ 𝑐 ( 𝑆 ∩ 𝑦 ) )
62 58 61 eqtr3id ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } = ∪ 𝑦 ∈ 𝑐 ( 𝑆 ∩ 𝑦 ) )
63 iunin2 ⊢ ∪ 𝑦 ∈ 𝑐 ( 𝑆 ∩ 𝑦 ) = ( 𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦 )
64 uniiun ⊢ ∪ 𝑐 = ∪ 𝑦 ∈ 𝑐 𝑦
65 64 eqcomi ⊢ ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐
66 65 a1i ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ∪ 𝑦 ∈ 𝑐 𝑦 = ∪ 𝑐 )
67 66 ineq2d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( 𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦 ) = ( 𝑆 ∩ ∪ 𝑐 ) )
68 incom ⊢ ( 𝑆 ∩ ∪ 𝑐 ) = ( ∪ 𝑐 ∩ 𝑆 )
69 sseqin2 ⊢ ( 𝑆 ⊆ ∪ 𝑐 ↔ ( ∪ 𝑐 ∩ 𝑆 ) = 𝑆 )
70 69 biimpi ⊢ ( 𝑆 ⊆ ∪ 𝑐 → ( ∪ 𝑐 ∩ 𝑆 ) = 𝑆 )
71 68 70 eqtrid ⊢ ( 𝑆 ⊆ ∪ 𝑐 → ( 𝑆 ∩ ∪ 𝑐 ) = 𝑆 )
72 71 adantl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( 𝑆 ∩ ∪ 𝑐 ) = 𝑆 )
73 67 72 eqtrd ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( 𝑆 ∩ ∪ 𝑦 ∈ 𝑐 𝑦 ) = 𝑆 )
74 63 73 eqtrid ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ∪ 𝑦 ∈ 𝑐 ( 𝑆 ∩ 𝑦 ) = 𝑆 )
75 62 74 eqtr2d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → 𝑆 = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } )
76 55 75 eqeq12d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( 𝑆 = 𝑆 ↔ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ) )
77 55 eqeq1d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( 𝑆 = ∪ 𝑡 ↔ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) )
78 77 rexbidv ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 ↔ ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) )
79 76 78 imbi12d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( ( 𝑆 = 𝑆 → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 ) ↔ ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
80 eqid ⊢ 𝑆 = 𝑆
81 80 a1bi ⊢ ( ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 ↔ ( 𝑆 = 𝑆 → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 ) )
82 elin ⊢ ( 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ↔ ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∧ 𝑡 ∈ Fin ) )
83 velpw ⊢ ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ 𝑡 ⊆ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } )
84 dfss3 ⊢ ( 𝑡 ⊆ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ ∀ 𝑠 ∈ 𝑡 𝑠 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } )
85 vex ⊢ 𝑠 ∈ V
86 eqeq1 ⊢ ( 𝑥 = 𝑠 → ( 𝑥 = ( 𝑦 ∩ 𝑆 ) ↔ 𝑠 = ( 𝑦 ∩ 𝑆 ) ) )
87 86 rexbidv ⊢ ( 𝑥 = 𝑠 → ( ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) ↔ ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ) )
88 85 87 elab ⊢ ( 𝑠 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) )
89 88 ralbii ⊢ ( ∀ 𝑠 ∈ 𝑡 𝑠 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) )
90 83 84 89 3bitri ⊢ ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ↔ ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) )
91 90 anbi1i ⊢ ( ( 𝑡 ∈ 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∧ 𝑡 ∈ Fin ) ↔ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) )
92 82 91 bitri ⊢ ( 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ↔ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) )
93 ineq1 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑠 ) → ( 𝑦 ∩ 𝑆 ) = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) )
94 93 eqeq2d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑠 ) → ( 𝑠 = ( 𝑦 ∩ 𝑆 ) ↔ 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) )
95 94 ac6sfi ⊢ ( ( 𝑡 ∈ Fin ∧ ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) )
96 95 ancoms ⊢ ( ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) )
97 96 adantl ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) )
98 frn ⊢ ( 𝑓 : 𝑡 ⟶ 𝑐 → ran 𝑓 ⊆ 𝑐 )
99 98 ad2antrl ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ⊆ 𝑐 )
100 vex ⊢ 𝑓 ∈ V
101 100 rnex ⊢ ran 𝑓 ∈ V
102 101 elpw ⊢ ( ran 𝑓 ∈ 𝒫 𝑐 ↔ ran 𝑓 ⊆ 𝑐 )
103 99 102 sylibr ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ∈ 𝒫 𝑐 )
104 simprr ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → 𝑡 ∈ Fin )
105 104 ad2antrr ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → 𝑡 ∈ Fin )
106 ffn ⊢ ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑓 Fn 𝑡 )
107 dffn4 ⊢ ( 𝑓 Fn 𝑡 ↔ 𝑓 : 𝑡 –onto→ ran 𝑓 )
108 106 107 sylib ⊢ ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑓 : 𝑡 –onto→ ran 𝑓 )
109 fodomfi ⊢ ( ( 𝑡 ∈ Fin ∧ 𝑓 : 𝑡 –onto→ ran 𝑓 ) → ran 𝑓 ≼ 𝑡 )
110 108 109 sylan2 ⊢ ( ( 𝑡 ∈ Fin ∧ 𝑓 : 𝑡 ⟶ 𝑐 ) → ran 𝑓 ≼ 𝑡 )
111 110 adantll ⊢ ( ( ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ∧ 𝑓 : 𝑡 ⟶ 𝑐 ) → ran 𝑓 ≼ 𝑡 )
112 111 adantll ⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑓 : 𝑡 ⟶ 𝑐 ) → ran 𝑓 ≼ 𝑡 )
113 112 ad2ant2r ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ≼ 𝑡 )
114 domfi ⊢ ( ( 𝑡 ∈ Fin ∧ ran 𝑓 ≼ 𝑡 ) → ran 𝑓 ∈ Fin )
115 105 113 114 syl2anc ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ∈ Fin )
116 103 115 elind ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) )
117 id ⊢ ( 𝑠 = 𝑢 → 𝑠 = 𝑢 )
118 fveq2 ⊢ ( 𝑠 = 𝑢 → ( 𝑓 ‘ 𝑠 ) = ( 𝑓 ‘ 𝑢 ) )
119 118 ineq1d ⊢ ( 𝑠 = 𝑢 → ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) )
120 117 119 eqeq12d ⊢ ( 𝑠 = 𝑢 → ( 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ↔ 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) )
121 120 rspccv ⊢ ( ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) → ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) )
122 pm2.27 ⊢ ( 𝑢 ∈ 𝑡 → ( ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) )
123 inss1 ⊢ ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ⊆ ( 𝑓 ‘ 𝑢 )
124 sseq1 ⊢ ( 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) → ( 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) ↔ ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ⊆ ( 𝑓 ‘ 𝑢 ) ) )
125 123 124 mpbiri ⊢ ( 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) → 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) )
126 ssel ⊢ ( 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) → ( 𝑤 ∈ 𝑢 → 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) )
127 126 a1dd ⊢ ( 𝑢 ⊆ ( 𝑓 ‘ 𝑢 ) → ( 𝑤 ∈ 𝑢 → ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) ) )
128 125 127 syl ⊢ ( 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) → ( 𝑤 ∈ 𝑢 → ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) ) )
129 128 a1i ⊢ ( 𝑢 ∈ 𝑡 → ( 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) → ( 𝑤 ∈ 𝑢 → ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) ) ) )
130 129 3imp ⊢ ( ( 𝑢 ∈ 𝑡 ∧ 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ∧ 𝑤 ∈ 𝑢 ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) )
131 fnfvelrn ⊢ ( ( 𝑓 Fn 𝑡 ∧ 𝑢 ∈ 𝑡 ) → ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 )
132 131 expcom ⊢ ( 𝑢 ∈ 𝑡 → ( 𝑓 Fn 𝑡 → ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) )
133 132 3ad2ant1 ⊢ ( ( 𝑢 ∈ 𝑡 ∧ 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ∧ 𝑤 ∈ 𝑢 ) → ( 𝑓 Fn 𝑡 → ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) )
134 106 133 syl5 ⊢ ( ( 𝑢 ∈ 𝑡 ∧ 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ∧ 𝑤 ∈ 𝑢 ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) )
135 130 134 jcad ⊢ ( ( 𝑢 ∈ 𝑡 ∧ 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ∧ 𝑤 ∈ 𝑢 ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) )
136 135 3exp ⊢ ( 𝑢 ∈ 𝑡 → ( 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) → ( 𝑤 ∈ 𝑢 → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) ) )
137 122 136 syld ⊢ ( 𝑢 ∈ 𝑡 → ( ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) → ( 𝑤 ∈ 𝑢 → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) ) )
138 137 com3r ⊢ ( 𝑤 ∈ 𝑢 → ( 𝑢 ∈ 𝑡 → ( ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) ) )
139 138 imp ⊢ ( ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ( ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) )
140 139 com3l ⊢ ( ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) → ( 𝑓 : 𝑡 ⟶ 𝑐 → ( ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) ) )
141 140 impcom ⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ( 𝑢 ∈ 𝑡 → 𝑢 = ( ( 𝑓 ‘ 𝑢 ) ∩ 𝑆 ) ) ) → ( ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) )
142 121 141 sylan2 ⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) )
143 fvex ⊢ ( 𝑓 ‘ 𝑢 ) ∈ V
144 eleq2 ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( 𝑤 ∈ 𝑣 ↔ 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ) )
145 eleq1 ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( 𝑣 ∈ ran 𝑓 ↔ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) )
146 144 145 anbi12d ⊢ ( 𝑣 = ( 𝑓 ‘ 𝑢 ) → ( ( 𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓 ) ↔ ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) ) )
147 143 146 spcev ⊢ ( ( 𝑤 ∈ ( 𝑓 ‘ 𝑢 ) ∧ ( 𝑓 ‘ 𝑢 ) ∈ ran 𝑓 ) → ∃ 𝑣 ( 𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓 ) )
148 142 147 syl6 ⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ∃ 𝑣 ( 𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓 ) ) )
149 148 exlimdv ⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( ∃ 𝑢 ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) → ∃ 𝑣 ( 𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓 ) ) )
150 eluni ⊢ ( 𝑤 ∈ ∪ 𝑡 ↔ ∃ 𝑢 ( 𝑤 ∈ 𝑢 ∧ 𝑢 ∈ 𝑡 ) )
151 eluni ⊢ ( 𝑤 ∈ ∪ ran 𝑓 ↔ ∃ 𝑣 ( 𝑤 ∈ 𝑣 ∧ 𝑣 ∈ ran 𝑓 ) )
152 149 150 151 3imtr4g ⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( 𝑤 ∈ ∪ 𝑡 → 𝑤 ∈ ∪ ran 𝑓 ) )
153 152 ssrdv ⊢ ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ∪ 𝑡 ⊆ ∪ ran 𝑓 )
154 153 adantl ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ∪ 𝑡 ⊆ ∪ ran 𝑓 )
155 sseq1 ⊢ ( 𝑆 = ∪ 𝑡 → ( 𝑆 ⊆ ∪ ran 𝑓 ↔ ∪ 𝑡 ⊆ ∪ ran 𝑓 ) )
156 155 ad2antlr ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ( 𝑆 ⊆ ∪ ran 𝑓 ↔ ∪ 𝑡 ⊆ ∪ ran 𝑓 ) )
157 154 156 mpbird ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → 𝑆 ⊆ ∪ ran 𝑓 )
158 116 157 jca ⊢ ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) ∧ ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) ) → ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) )
159 158 ex ⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) → ( ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) ) )
160 159 eximdv ⊢ ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) ∧ 𝑆 = ∪ 𝑡 ) → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) ) )
161 160 ex ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( 𝑆 = ∪ 𝑡 → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) ) ) )
162 161 com23 ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( 𝑆 = ∪ 𝑡 → ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) ) ) )
163 unieq ⊢ ( 𝑑 = ran 𝑓 → ∪ 𝑑 = ∪ ran 𝑓 )
164 163 sseq2d ⊢ ( 𝑑 = ran 𝑓 → ( 𝑆 ⊆ ∪ 𝑑 ↔ 𝑆 ⊆ ∪ ran 𝑓 ) )
165 164 rspcev ⊢ ( ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 )
166 165 exlimiv ⊢ ( ∃ 𝑓 ( ran 𝑓 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑆 ⊆ ∪ ran 𝑓 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 )
167 162 166 syl8 ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑡 ⟶ 𝑐 ∧ ∀ 𝑠 ∈ 𝑡 𝑠 = ( ( 𝑓 ‘ 𝑠 ) ∩ 𝑆 ) ) → ( 𝑆 = ∪ 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) )
168 97 167 mpd ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ ( ∀ 𝑠 ∈ 𝑡 ∃ 𝑦 ∈ 𝑐 𝑠 = ( 𝑦 ∩ 𝑆 ) ∧ 𝑡 ∈ Fin ) ) → ( 𝑆 = ∪ 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) )
169 92 168 sylan2b ⊢ ( ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) ∧ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ) → ( 𝑆 = ∪ 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) )
170 169 rexlimdva ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) )
171 81 170 biimtrrid ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( ( 𝑆 = 𝑆 → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) 𝑆 = ∪ 𝑡 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) )
172 79 171 sylbird ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) ∧ 𝑆 ⊆ ∪ 𝑐 ) → ( ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) )
173 172 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( 𝑆 ⊆ ∪ 𝑐 → ( ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) )
174 173 com23 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } → ∃ 𝑡 ∈ ( 𝒫 { 𝑥 ∣ ∃ 𝑦 ∈ 𝑐 𝑥 = ( 𝑦 ∩ 𝑆 ) } ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) )
175 53 174 syld ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑐 ∈ 𝒫 𝐽 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) )
176 175 ralrimdva ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) → ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) )
177 1 cmpsublem ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
178 176 177 impbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) )
179 13 178 bitrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ↔ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) )