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

Metamath Proof Explorer

Theorem cmpsublem

Description: Lemma for cmpsub . (Contributed by Jeff Hankins, 28-Jun-2009)

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

Proof

Step Hyp Ref Expression
1 cmpsub.1 ⊢ 𝑋 = ∪ 𝐽
2 rabexg ⊢ ( 𝐽 ∈ Top → { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∈ V )
3 2 ad2antrr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) → { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∈ V )
4 ssrab2 ⊢ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ⊆ 𝐽
5 elpwg ⊢ ( { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∈ V → ( { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∈ 𝒫 𝐽 ↔ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ⊆ 𝐽 ) )
6 4 5 mpbiri ⊢ ( { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∈ V → { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∈ 𝒫 𝐽 )
7 3 6 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) → { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∈ 𝒫 𝐽 )
8 unieq ⊢ ( 𝑐 = { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∪ 𝑐 = ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } )
9 8 sseq2d ⊢ ( 𝑐 = { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ( 𝑆 ⊆ ∪ 𝑐 ↔ 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) )
10 pweq ⊢ ( 𝑐 = { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → 𝒫 𝑐 = 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } )
11 10 ineq1d ⊢ ( 𝑐 = { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ( 𝒫 𝑐 ∩ Fin ) = ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) )
12 11 rexeqdv ⊢ ( 𝑐 = { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ( ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ↔ ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) )
13 9 12 imbi12d ⊢ ( 𝑐 = { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ( ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ↔ ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) )
14 13 rspcva ⊢ ( ( { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∈ 𝒫 𝐽 ∧ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) → ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) )
15 7 14 sylan ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) → ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) )
16 15 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) ) )
17 1 restuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) )
18 17 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) )
19 18 eqeq1d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) → ( 𝑆 = ∪ 𝑠 ↔ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 ) )
20 velpw ⊢ ( 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ↔ 𝑠 ⊆ ( 𝐽 ↾t 𝑆 ) )
21 eleq2 ⊢ ( 𝑆 = ∪ 𝑠 → ( 𝑡 ∈ 𝑆 ↔ 𝑡 ∈ ∪ 𝑠 ) )
22 eluni ⊢ ( 𝑡 ∈ ∪ 𝑠 ↔ ∃ 𝑢 ( 𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠 ) )
23 21 22 bitrdi ⊢ ( 𝑆 = ∪ 𝑠 → ( 𝑡 ∈ 𝑆 ↔ ∃ 𝑢 ( 𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠 ) ) )
24 23 adantl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ⊆ ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ( 𝑡 ∈ 𝑆 ↔ ∃ 𝑢 ( 𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠 ) ) )
25 ssel ⊢ ( 𝑠 ⊆ ( 𝐽 ↾t 𝑆 ) → ( 𝑢 ∈ 𝑠 → 𝑢 ∈ ( 𝐽 ↾t 𝑆 ) ) )
26 1 sseq2i ⊢ ( 𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽 )
27 uniexg ⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ V )
28 ssexg ⊢ ( ( 𝑆 ⊆ ∪ 𝐽 ∧ ∪ 𝐽 ∈ V ) → 𝑆 ∈ V )
29 28 ancoms ⊢ ( ( ∪ 𝐽 ∈ V ∧ 𝑆 ⊆ ∪ 𝐽 ) → 𝑆 ∈ V )
30 27 29 sylan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → 𝑆 ∈ V )
31 26 30 sylan2b ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ V )
32 elrest ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ∈ V ) → ( 𝑢 ∈ ( 𝐽 ↾t 𝑆 ) ↔ ∃ 𝑤 ∈ 𝐽 𝑢 = ( 𝑤 ∩ 𝑆 ) ) )
33 31 32 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑢 ∈ ( 𝐽 ↾t 𝑆 ) ↔ ∃ 𝑤 ∈ 𝐽 𝑢 = ( 𝑤 ∩ 𝑆 ) ) )
34 inss1 ⊢ ( 𝑤 ∩ 𝑆 ) ⊆ 𝑤
35 sseq1 ⊢ ( 𝑢 = ( 𝑤 ∩ 𝑆 ) → ( 𝑢 ⊆ 𝑤 ↔ ( 𝑤 ∩ 𝑆 ) ⊆ 𝑤 ) )
36 34 35 mpbiri ⊢ ( 𝑢 = ( 𝑤 ∩ 𝑆 ) → 𝑢 ⊆ 𝑤 )
37 36 sselda ⊢ ( ( 𝑢 = ( 𝑤 ∩ 𝑆 ) ∧ 𝑡 ∈ 𝑢 ) → 𝑡 ∈ 𝑤 )
38 37 3ad2antl3 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = ( 𝑤 ∩ 𝑆 ) ) ∧ 𝑡 ∈ 𝑢 ) → 𝑡 ∈ 𝑤 )
39 38 3adant2 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = ( 𝑤 ∩ 𝑆 ) ) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢 ) → 𝑡 ∈ 𝑤 )
40 ineq1 ⊢ ( 𝑦 = 𝑤 → ( 𝑦 ∩ 𝑆 ) = ( 𝑤 ∩ 𝑆 ) )
41 40 eleq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 ↔ ( 𝑤 ∩ 𝑆 ) ∈ 𝑠 ) )
42 simp12 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = ( 𝑤 ∩ 𝑆 ) ) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢 ) → 𝑤 ∈ 𝐽 )
43 eleq1 ⊢ ( 𝑢 = ( 𝑤 ∩ 𝑆 ) → ( 𝑢 ∈ 𝑠 ↔ ( 𝑤 ∩ 𝑆 ) ∈ 𝑠 ) )
44 43 biimpa ⊢ ( ( 𝑢 = ( 𝑤 ∩ 𝑆 ) ∧ 𝑢 ∈ 𝑠 ) → ( 𝑤 ∩ 𝑆 ) ∈ 𝑠 )
45 44 3ad2antl3 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = ( 𝑤 ∩ 𝑆 ) ) ∧ 𝑢 ∈ 𝑠 ) → ( 𝑤 ∩ 𝑆 ) ∈ 𝑠 )
46 45 3adant3 ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = ( 𝑤 ∩ 𝑆 ) ) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢 ) → ( 𝑤 ∩ 𝑆 ) ∈ 𝑠 )
47 41 42 46 elrabd ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = ( 𝑤 ∩ 𝑆 ) ) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢 ) → 𝑤 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } )
48 vex ⊢ 𝑤 ∈ V
49 eleq2 ⊢ ( 𝑣 = 𝑤 → ( 𝑡 ∈ 𝑣 ↔ 𝑡 ∈ 𝑤 ) )
50 eleq1 ⊢ ( 𝑣 = 𝑤 → ( 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ↔ 𝑤 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) )
51 49 50 anbi12d ⊢ ( 𝑣 = 𝑤 → ( ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ↔ ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) )
52 48 51 spcev ⊢ ( ( 𝑡 ∈ 𝑤 ∧ 𝑤 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) )
53 39 47 52 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = ( 𝑤 ∩ 𝑆 ) ) ∧ 𝑢 ∈ 𝑠 ∧ 𝑡 ∈ 𝑢 ) → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) )
54 53 3exp ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑤 ∈ 𝐽 ∧ 𝑢 = ( 𝑤 ∩ 𝑆 ) ) → ( 𝑢 ∈ 𝑠 → ( 𝑡 ∈ 𝑢 → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) ) )
55 54 rexlimdv3a ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∃ 𝑤 ∈ 𝐽 𝑢 = ( 𝑤 ∩ 𝑆 ) → ( 𝑢 ∈ 𝑠 → ( 𝑡 ∈ 𝑢 → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) ) ) )
56 33 55 sylbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑢 ∈ ( 𝐽 ↾t 𝑆 ) → ( 𝑢 ∈ 𝑠 → ( 𝑡 ∈ 𝑢 → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) ) ) )
57 56 com23 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑢 ∈ 𝑠 → ( 𝑢 ∈ ( 𝐽 ↾t 𝑆 ) → ( 𝑡 ∈ 𝑢 → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) ) ) )
58 57 com4l ⊢ ( 𝑢 ∈ 𝑠 → ( 𝑢 ∈ ( 𝐽 ↾t 𝑆 ) → ( 𝑡 ∈ 𝑢 → ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) ) ) )
59 25 58 sylcom ⊢ ( 𝑠 ⊆ ( 𝐽 ↾t 𝑆 ) → ( 𝑢 ∈ 𝑠 → ( 𝑡 ∈ 𝑢 → ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) ) ) )
60 59 com24 ⊢ ( 𝑠 ⊆ ( 𝐽 ↾t 𝑆 ) → ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑡 ∈ 𝑢 → ( 𝑢 ∈ 𝑠 → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) ) ) )
61 60 impcom ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ⊆ ( 𝐽 ↾t 𝑆 ) ) → ( 𝑡 ∈ 𝑢 → ( 𝑢 ∈ 𝑠 → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) ) )
62 61 impd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ⊆ ( 𝐽 ↾t 𝑆 ) ) → ( ( 𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠 ) → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) )
63 62 exlimdv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ⊆ ( 𝐽 ↾t 𝑆 ) ) → ( ∃ 𝑢 ( 𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠 ) → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) )
64 63 adantr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ⊆ ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ( ∃ 𝑢 ( 𝑡 ∈ 𝑢 ∧ 𝑢 ∈ 𝑠 ) → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) )
65 24 64 sylbid ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ⊆ ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ( 𝑡 ∈ 𝑆 → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) )
66 65 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ⊆ ( 𝐽 ↾t 𝑆 ) ) → ( 𝑆 = ∪ 𝑠 → ( 𝑡 ∈ 𝑆 → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) ) )
67 20 66 sylan2b ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) → ( 𝑆 = ∪ 𝑠 → ( 𝑡 ∈ 𝑆 → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) ) )
68 67 imp ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ( 𝑡 ∈ 𝑆 → ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) ) )
69 eluni ⊢ ( 𝑡 ∈ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ↔ ∃ 𝑣 ( 𝑡 ∈ 𝑣 ∧ 𝑣 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) )
70 68 69 imbitrrdi ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ( 𝑡 ∈ 𝑆 → 𝑡 ∈ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) )
71 70 ssrdv ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } )
72 pm2.27 ⊢ ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ( ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) )
73 elin ⊢ ( 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) ↔ ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) )
74 vex ⊢ 𝑡 ∈ V
75 eqeq1 ⊢ ( 𝑥 = 𝑡 → ( 𝑥 = ( 𝑧 ∩ 𝑆 ) ↔ 𝑡 = ( 𝑧 ∩ 𝑆 ) ) )
76 75 rexbidv ⊢ ( 𝑥 = 𝑡 → ( ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) ↔ ∃ 𝑧 ∈ 𝑑 𝑡 = ( 𝑧 ∩ 𝑆 ) ) )
77 74 76 elab ⊢ ( 𝑡 ∈ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ↔ ∃ 𝑧 ∈ 𝑑 𝑡 = ( 𝑧 ∩ 𝑆 ) )
78 velpw ⊢ ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ↔ 𝑑 ⊆ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } )
79 ssel ⊢ ( 𝑑 ⊆ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ( 𝑧 ∈ 𝑑 → 𝑧 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ) )
80 ineq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∩ 𝑆 ) = ( 𝑧 ∩ 𝑆 ) )
81 80 eleq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 ↔ ( 𝑧 ∩ 𝑆 ) ∈ 𝑠 ) )
82 81 elrab ⊢ ( 𝑧 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ↔ ( 𝑧 ∈ 𝐽 ∧ ( 𝑧 ∩ 𝑆 ) ∈ 𝑠 ) )
83 eleq1a ⊢ ( ( 𝑧 ∩ 𝑆 ) ∈ 𝑠 → ( 𝑡 = ( 𝑧 ∩ 𝑆 ) → 𝑡 ∈ 𝑠 ) )
84 82 83 simplbiim ⊢ ( 𝑧 ∈ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ( 𝑡 = ( 𝑧 ∩ 𝑆 ) → 𝑡 ∈ 𝑠 ) )
85 79 84 syl6 ⊢ ( 𝑑 ⊆ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ( 𝑧 ∈ 𝑑 → ( 𝑡 = ( 𝑧 ∩ 𝑆 ) → 𝑡 ∈ 𝑠 ) ) )
86 85 2a1d ⊢ ( 𝑑 ⊆ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ( 𝑆 ⊆ ∪ 𝑑 → ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ( 𝑧 ∈ 𝑑 → ( 𝑡 = ( 𝑧 ∩ 𝑆 ) → 𝑡 ∈ 𝑠 ) ) ) ) )
87 86 adantr ⊢ ( ( 𝑑 ⊆ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) → ( 𝑆 ⊆ ∪ 𝑑 → ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ( 𝑧 ∈ 𝑑 → ( 𝑡 = ( 𝑧 ∩ 𝑆 ) → 𝑡 ∈ 𝑠 ) ) ) ) )
88 78 87 sylanb ⊢ ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) → ( 𝑆 ⊆ ∪ 𝑑 → ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ( 𝑧 ∈ 𝑑 → ( 𝑡 = ( 𝑧 ∩ 𝑆 ) → 𝑡 ∈ 𝑠 ) ) ) ) )
89 88 3imp ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → ( 𝑧 ∈ 𝑑 → ( 𝑡 = ( 𝑧 ∩ 𝑆 ) → 𝑡 ∈ 𝑠 ) ) )
90 89 rexlimdv ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → ( ∃ 𝑧 ∈ 𝑑 𝑡 = ( 𝑧 ∩ 𝑆 ) → 𝑡 ∈ 𝑠 ) )
91 77 90 biimtrid ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → ( 𝑡 ∈ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } → 𝑡 ∈ 𝑠 ) )
92 91 ssrdv ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ⊆ 𝑠 )
93 vex ⊢ 𝑑 ∈ V
94 93 abrexex ⊢ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ∈ V
95 94 elpw ⊢ ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ∈ 𝒫 𝑠 ↔ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ⊆ 𝑠 )
96 92 95 sylibr ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ∈ 𝒫 𝑠 )
97 abrexfi ⊢ ( 𝑑 ∈ Fin → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ∈ Fin )
98 97 ad2antlr ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ∈ Fin )
99 98 3adant3 ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ∈ Fin )
100 96 99 elind ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ∈ ( 𝒫 𝑠 ∩ Fin ) )
101 dfss ⊢ ( 𝑆 ⊆ ∪ 𝑑 ↔ 𝑆 = ( 𝑆 ∩ ∪ 𝑑 ) )
102 101 biimpi ⊢ ( 𝑆 ⊆ ∪ 𝑑 → 𝑆 = ( 𝑆 ∩ ∪ 𝑑 ) )
103 uniiun ⊢ ∪ 𝑑 = ∪ 𝑧 ∈ 𝑑 𝑧
104 103 ineq2i ⊢ ( 𝑆 ∩ ∪ 𝑑 ) = ( 𝑆 ∩ ∪ 𝑧 ∈ 𝑑 𝑧 )
105 iunin2 ⊢ ∪ 𝑧 ∈ 𝑑 ( 𝑆 ∩ 𝑧 ) = ( 𝑆 ∩ ∪ 𝑧 ∈ 𝑑 𝑧 )
106 incom ⊢ ( 𝑆 ∩ 𝑧 ) = ( 𝑧 ∩ 𝑆 )
107 106 a1i ⊢ ( 𝑧 ∈ 𝑑 → ( 𝑆 ∩ 𝑧 ) = ( 𝑧 ∩ 𝑆 ) )
108 107 iuneq2i ⊢ ∪ 𝑧 ∈ 𝑑 ( 𝑆 ∩ 𝑧 ) = ∪ 𝑧 ∈ 𝑑 ( 𝑧 ∩ 𝑆 )
109 104 105 108 3eqtr2i ⊢ ( 𝑆 ∩ ∪ 𝑑 ) = ∪ 𝑧 ∈ 𝑑 ( 𝑧 ∩ 𝑆 )
110 102 109 eqtrdi ⊢ ( 𝑆 ⊆ ∪ 𝑑 → 𝑆 = ∪ 𝑧 ∈ 𝑑 ( 𝑧 ∩ 𝑆 ) )
111 110 3ad2ant2 ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → 𝑆 = ∪ 𝑧 ∈ 𝑑 ( 𝑧 ∩ 𝑆 ) )
112 18 ad2antrl ⊢ ( ( 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) )
113 112 3adant1 ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → 𝑆 = ∪ ( 𝐽 ↾t 𝑆 ) )
114 vex ⊢ 𝑧 ∈ V
115 114 inex1 ⊢ ( 𝑧 ∩ 𝑆 ) ∈ V
116 115 dfiun2 ⊢ ∪ 𝑧 ∈ 𝑑 ( 𝑧 ∩ 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) }
117 116 a1i ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → ∪ 𝑧 ∈ 𝑑 ( 𝑧 ∩ 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } )
118 111 113 117 3eqtr3d ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } )
119 unieq ⊢ ( 𝑡 = { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } → ∪ 𝑡 = ∪ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } )
120 119 rspceeqv ⊢ ( ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ∈ ( 𝒫 𝑠 ∩ Fin ) ∧ ∪ ( 𝐽 ↾t 𝑆 ) = ∪ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑑 𝑥 = ( 𝑧 ∩ 𝑆 ) } ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 )
121 100 118 120 syl2anc ⊢ ( ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) ∧ 𝑆 ⊆ ∪ 𝑑 ∧ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 )
122 121 3exp ⊢ ( ( 𝑑 ∈ 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∧ 𝑑 ∈ Fin ) → ( 𝑆 ⊆ ∪ 𝑑 → ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
123 73 122 sylbi ⊢ ( 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) → ( 𝑆 ⊆ ∪ 𝑑 → ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
124 123 rexlimiv ⊢ ( ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 → ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) )
125 72 124 syl6 ⊢ ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ( ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
126 125 com3r ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ( ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
127 71 126 mpd ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) ∧ 𝑆 = ∪ 𝑠 ) → ( ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) )
128 127 ex ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) → ( 𝑆 = ∪ 𝑠 → ( ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
129 19 128 sylbird ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) → ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ( ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
130 129 com23 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) → ( ( 𝑆 ⊆ ∪ { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } → ∃ 𝑑 ∈ ( 𝒫 { 𝑦 ∈ 𝐽 ∣ ( 𝑦 ∩ 𝑆 ) ∈ 𝑠 } ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
131 16 130 syld ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )
132 131 ralrimdva ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑑 ) → ∀ 𝑠 ∈ 𝒫 ( 𝐽 ↾t 𝑆 ) ( ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑠 → ∃ 𝑡 ∈ ( 𝒫 𝑠 ∩ Fin ) ∪ ( 𝐽 ↾t 𝑆 ) = ∪ 𝑡 ) ) )