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

Metamath Proof Explorer

Theorem uncmp

Description: The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010)

Ref Expression
Hypothesis uncmp.1 ⊢ 𝑋 = ∪ 𝐽
Assertion uncmp ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ∧ ( 𝐽 ↾t 𝑇 ) ∈ Comp ) ) → 𝐽 ∈ Comp )

Proof

Step Hyp Ref Expression
1 uncmp.1 ⊢ 𝑋 = ∪ 𝐽
2 simpll ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ∧ ( 𝐽 ↾t 𝑇 ) ∈ Comp ) ) → 𝐽 ∈ Top )
3 simpll ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → 𝐽 ∈ Top )
4 ssun1 ⊢ 𝑆 ⊆ ( 𝑆 ∪ 𝑇 )
5 sseq2 ⊢ ( 𝑋 = ( 𝑆 ∪ 𝑇 ) → ( 𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ( 𝑆 ∪ 𝑇 ) ) )
6 4 5 mpbiri ⊢ ( 𝑋 = ( 𝑆 ∪ 𝑇 ) → 𝑆 ⊆ 𝑋 )
7 6 ad2antlr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → 𝑆 ⊆ 𝑋 )
8 1 cmpsub ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ↔ ∀ 𝑚 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑚 → ∃ 𝑛 ∈ ( 𝒫 𝑚 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) ) )
9 3 7 8 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ↔ ∀ 𝑚 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑚 → ∃ 𝑛 ∈ ( 𝒫 𝑚 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) ) )
10 simprr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → 𝑋 = ∪ 𝑐 )
11 7 10 sseqtrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → 𝑆 ⊆ ∪ 𝑐 )
12 unieq ⊢ ( 𝑚 = 𝑐 → ∪ 𝑚 = ∪ 𝑐 )
13 12 sseq2d ⊢ ( 𝑚 = 𝑐 → ( 𝑆 ⊆ ∪ 𝑚 ↔ 𝑆 ⊆ ∪ 𝑐 ) )
14 pweq ⊢ ( 𝑚 = 𝑐 → 𝒫 𝑚 = 𝒫 𝑐 )
15 14 ineq1d ⊢ ( 𝑚 = 𝑐 → ( 𝒫 𝑚 ∩ Fin ) = ( 𝒫 𝑐 ∩ Fin ) )
16 15 rexeqdv ⊢ ( 𝑚 = 𝑐 → ( ∃ 𝑛 ∈ ( 𝒫 𝑚 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ↔ ∃ 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) )
17 13 16 imbi12d ⊢ ( 𝑚 = 𝑐 → ( ( 𝑆 ⊆ ∪ 𝑚 → ∃ 𝑛 ∈ ( 𝒫 𝑚 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) ↔ ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) ) )
18 17 rspcv ⊢ ( 𝑐 ∈ 𝒫 𝐽 → ( ∀ 𝑚 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑚 → ∃ 𝑛 ∈ ( 𝒫 𝑚 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) → ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) ) )
19 18 ad2antrl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ∀ 𝑚 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑚 → ∃ 𝑛 ∈ ( 𝒫 𝑚 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) → ( 𝑆 ⊆ ∪ 𝑐 → ∃ 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) ) )
20 11 19 mpid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ∀ 𝑚 ∈ 𝒫 𝐽 ( 𝑆 ⊆ ∪ 𝑚 → ∃ 𝑛 ∈ ( 𝒫 𝑚 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) → ∃ 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) )
21 9 20 sylbid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Comp → ∃ 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ) )
22 ssun2 ⊢ 𝑇 ⊆ ( 𝑆 ∪ 𝑇 )
23 sseq2 ⊢ ( 𝑋 = ( 𝑆 ∪ 𝑇 ) → ( 𝑇 ⊆ 𝑋 ↔ 𝑇 ⊆ ( 𝑆 ∪ 𝑇 ) ) )
24 22 23 mpbiri ⊢ ( 𝑋 = ( 𝑆 ∪ 𝑇 ) → 𝑇 ⊆ 𝑋 )
25 24 ad2antlr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → 𝑇 ⊆ 𝑋 )
26 1 cmpsub ⊢ ( ( 𝐽 ∈ Top ∧ 𝑇 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑇 ) ∈ Comp ↔ ∀ 𝑟 ∈ 𝒫 𝐽 ( 𝑇 ⊆ ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) ) )
27 3 25 26 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ( 𝐽 ↾t 𝑇 ) ∈ Comp ↔ ∀ 𝑟 ∈ 𝒫 𝐽 ( 𝑇 ⊆ ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) ) )
28 25 10 sseqtrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → 𝑇 ⊆ ∪ 𝑐 )
29 unieq ⊢ ( 𝑟 = 𝑐 → ∪ 𝑟 = ∪ 𝑐 )
30 29 sseq2d ⊢ ( 𝑟 = 𝑐 → ( 𝑇 ⊆ ∪ 𝑟 ↔ 𝑇 ⊆ ∪ 𝑐 ) )
31 pweq ⊢ ( 𝑟 = 𝑐 → 𝒫 𝑟 = 𝒫 𝑐 )
32 31 ineq1d ⊢ ( 𝑟 = 𝑐 → ( 𝒫 𝑟 ∩ Fin ) = ( 𝒫 𝑐 ∩ Fin ) )
33 32 rexeqdv ⊢ ( 𝑟 = 𝑐 → ( ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ↔ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) )
34 30 33 imbi12d ⊢ ( 𝑟 = 𝑐 → ( ( 𝑇 ⊆ ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) ↔ ( 𝑇 ⊆ ∪ 𝑐 → ∃ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) ) )
35 34 rspcv ⊢ ( 𝑐 ∈ 𝒫 𝐽 → ( ∀ 𝑟 ∈ 𝒫 𝐽 ( 𝑇 ⊆ ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) → ( 𝑇 ⊆ ∪ 𝑐 → ∃ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) ) )
36 35 ad2antrl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ∀ 𝑟 ∈ 𝒫 𝐽 ( 𝑇 ⊆ ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) → ( 𝑇 ⊆ ∪ 𝑐 → ∃ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) ) )
37 28 36 mpid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ∀ 𝑟 ∈ 𝒫 𝐽 ( 𝑇 ⊆ ∪ 𝑟 → ∃ 𝑠 ∈ ( 𝒫 𝑟 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) → ∃ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) )
38 27 37 sylbid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ( 𝐽 ↾t 𝑇 ) ∈ Comp → ∃ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) )
39 reeanv ⊢ ( ∃ 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∃ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ↔ ( ∃ 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) )
40 elinel1 ⊢ ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) → 𝑛 ∈ 𝒫 𝑐 )
41 40 elpwid ⊢ ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) → 𝑛 ⊆ 𝑐 )
42 elinel1 ⊢ ( 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) → 𝑠 ∈ 𝒫 𝑐 )
43 42 elpwid ⊢ ( 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) → 𝑠 ⊆ 𝑐 )
44 41 43 anim12i ⊢ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) → ( 𝑛 ⊆ 𝑐 ∧ 𝑠 ⊆ 𝑐 ) )
45 44 ad2antrl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → ( 𝑛 ⊆ 𝑐 ∧ 𝑠 ⊆ 𝑐 ) )
46 unss ⊢ ( ( 𝑛 ⊆ 𝑐 ∧ 𝑠 ⊆ 𝑐 ) ↔ ( 𝑛 ∪ 𝑠 ) ⊆ 𝑐 )
47 45 46 sylib ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → ( 𝑛 ∪ 𝑠 ) ⊆ 𝑐 )
48 elinel2 ⊢ ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) → 𝑛 ∈ Fin )
49 elinel2 ⊢ ( 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) → 𝑠 ∈ Fin )
50 unfi ⊢ ( ( 𝑛 ∈ Fin ∧ 𝑠 ∈ Fin ) → ( 𝑛 ∪ 𝑠 ) ∈ Fin )
51 48 49 50 syl2an ⊢ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) → ( 𝑛 ∪ 𝑠 ) ∈ Fin )
52 51 ad2antrl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → ( 𝑛 ∪ 𝑠 ) ∈ Fin )
53 47 52 jca ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → ( ( 𝑛 ∪ 𝑠 ) ⊆ 𝑐 ∧ ( 𝑛 ∪ 𝑠 ) ∈ Fin ) )
54 elin ⊢ ( ( 𝑛 ∪ 𝑠 ) ∈ ( 𝒫 𝑐 ∩ Fin ) ↔ ( ( 𝑛 ∪ 𝑠 ) ∈ 𝒫 𝑐 ∧ ( 𝑛 ∪ 𝑠 ) ∈ Fin ) )
55 vex ⊢ 𝑐 ∈ V
56 55 elpw2 ⊢ ( ( 𝑛 ∪ 𝑠 ) ∈ 𝒫 𝑐 ↔ ( 𝑛 ∪ 𝑠 ) ⊆ 𝑐 )
57 56 anbi1i ⊢ ( ( ( 𝑛 ∪ 𝑠 ) ∈ 𝒫 𝑐 ∧ ( 𝑛 ∪ 𝑠 ) ∈ Fin ) ↔ ( ( 𝑛 ∪ 𝑠 ) ⊆ 𝑐 ∧ ( 𝑛 ∪ 𝑠 ) ∈ Fin ) )
58 54 57 bitr2i ⊢ ( ( ( 𝑛 ∪ 𝑠 ) ⊆ 𝑐 ∧ ( 𝑛 ∪ 𝑠 ) ∈ Fin ) ↔ ( 𝑛 ∪ 𝑠 ) ∈ ( 𝒫 𝑐 ∩ Fin ) )
59 53 58 sylib ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → ( 𝑛 ∪ 𝑠 ) ∈ ( 𝒫 𝑐 ∩ Fin ) )
60 simpllr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → 𝑋 = ( 𝑆 ∪ 𝑇 ) )
61 ssun3 ⊢ ( 𝑆 ⊆ ∪ 𝑛 → 𝑆 ⊆ ( ∪ 𝑛 ∪ ∪ 𝑠 ) )
62 ssun4 ⊢ ( 𝑇 ⊆ ∪ 𝑠 → 𝑇 ⊆ ( ∪ 𝑛 ∪ ∪ 𝑠 ) )
63 61 62 anim12i ⊢ ( ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) → ( 𝑆 ⊆ ( ∪ 𝑛 ∪ ∪ 𝑠 ) ∧ 𝑇 ⊆ ( ∪ 𝑛 ∪ ∪ 𝑠 ) ) )
64 63 ad2antll ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → ( 𝑆 ⊆ ( ∪ 𝑛 ∪ ∪ 𝑠 ) ∧ 𝑇 ⊆ ( ∪ 𝑛 ∪ ∪ 𝑠 ) ) )
65 unss ⊢ ( ( 𝑆 ⊆ ( ∪ 𝑛 ∪ ∪ 𝑠 ) ∧ 𝑇 ⊆ ( ∪ 𝑛 ∪ ∪ 𝑠 ) ) ↔ ( 𝑆 ∪ 𝑇 ) ⊆ ( ∪ 𝑛 ∪ ∪ 𝑠 ) )
66 64 65 sylib ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → ( 𝑆 ∪ 𝑇 ) ⊆ ( ∪ 𝑛 ∪ ∪ 𝑠 ) )
67 60 66 eqsstrd ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → 𝑋 ⊆ ( ∪ 𝑛 ∪ ∪ 𝑠 ) )
68 uniun ⊢ ∪ ( 𝑛 ∪ 𝑠 ) = ( ∪ 𝑛 ∪ ∪ 𝑠 )
69 67 68 sseqtrrdi ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → 𝑋 ⊆ ∪ ( 𝑛 ∪ 𝑠 ) )
70 elpwi ⊢ ( 𝑐 ∈ 𝒫 𝐽 → 𝑐 ⊆ 𝐽 )
71 70 adantr ⊢ ( ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → 𝑐 ⊆ 𝐽 )
72 71 ad2antlr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → 𝑐 ⊆ 𝐽 )
73 47 72 sstrd ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → ( 𝑛 ∪ 𝑠 ) ⊆ 𝐽 )
74 uniss ⊢ ( ( 𝑛 ∪ 𝑠 ) ⊆ 𝐽 → ∪ ( 𝑛 ∪ 𝑠 ) ⊆ ∪ 𝐽 )
75 74 1 sseqtrrdi ⊢ ( ( 𝑛 ∪ 𝑠 ) ⊆ 𝐽 → ∪ ( 𝑛 ∪ 𝑠 ) ⊆ 𝑋 )
76 73 75 syl ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → ∪ ( 𝑛 ∪ 𝑠 ) ⊆ 𝑋 )
77 69 76 eqssd ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → 𝑋 = ∪ ( 𝑛 ∪ 𝑠 ) )
78 unieq ⊢ ( 𝑑 = ( 𝑛 ∪ 𝑠 ) → ∪ 𝑑 = ∪ ( 𝑛 ∪ 𝑠 ) )
79 78 rspceeqv ⊢ ( ( ( 𝑛 ∪ 𝑠 ) ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑋 = ∪ ( 𝑛 ∪ 𝑠 ) ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 )
80 59 77 79 syl2anc ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) ∧ ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) ∧ ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) ) ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 )
81 80 exp32 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ( 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∧ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ) → ( ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
82 81 rexlimdvv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ∃ 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) ∃ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) ( 𝑆 ⊆ ∪ 𝑛 ∧ 𝑇 ⊆ ∪ 𝑠 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
83 39 82 biimtrrid ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ( ∃ 𝑛 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑆 ⊆ ∪ 𝑛 ∧ ∃ 𝑠 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑇 ⊆ ∪ 𝑠 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
84 21 38 83 syl2and ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) ) → ( ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ∧ ( 𝐽 ↾t 𝑇 ) ∈ Comp ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
85 84 impancom ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ∧ ( 𝐽 ↾t 𝑇 ) ∈ Comp ) ) → ( ( 𝑐 ∈ 𝒫 𝐽 ∧ 𝑋 = ∪ 𝑐 ) → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
86 85 expd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ∧ ( 𝐽 ↾t 𝑇 ) ∈ Comp ) ) → ( 𝑐 ∈ 𝒫 𝐽 → ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
87 86 ralrimiv ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ∧ ( 𝐽 ↾t 𝑇 ) ∈ Comp ) ) → ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) )
88 1 iscmp ⊢ ( 𝐽 ∈ Comp ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ 𝒫 𝐽 ( 𝑋 = ∪ 𝑐 → ∃ 𝑑 ∈ ( 𝒫 𝑐 ∩ Fin ) 𝑋 = ∪ 𝑑 ) ) )
89 2 87 88 sylanbrc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑋 = ( 𝑆 ∪ 𝑇 ) ) ∧ ( ( 𝐽 ↾t 𝑆 ) ∈ Comp ∧ ( 𝐽 ↾t 𝑇 ) ∈ Comp ) ) → 𝐽 ∈ Comp )