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 syl5bir ( ( ( 𝐽 ∈ 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 )