Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  uncmp Structured version   Visualization version   GIF version

Theorem uncmp 22005
 Description: The union of two compact sets is compact. (Contributed by Jeff Hankins, 30-Jan-2010.)
Hypothesis
Ref Expression
uncmp.1 𝑋 = 𝐽
Assertion
Ref Expression
uncmp (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → 𝐽 ∈ Comp)

Proof of Theorem uncmp
Dummy variables 𝑐 𝑑 𝑚 𝑛 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpll 765 . 2 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → 𝐽 ∈ Top)
2 simpll 765 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝐽 ∈ Top)
3 ssun1 4148 . . . . . . . . . 10 𝑆 ⊆ (𝑆𝑇)
4 sseq2 3993 . . . . . . . . . 10 (𝑋 = (𝑆𝑇) → (𝑆𝑋𝑆 ⊆ (𝑆𝑇)))
53, 4mpbiri 260 . . . . . . . . 9 (𝑋 = (𝑆𝑇) → 𝑆𝑋)
65ad2antlr 725 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑆𝑋)
7 uncmp.1 . . . . . . . . 9 𝑋 = 𝐽
87cmpsub 22002 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛)))
92, 6, 8syl2anc 586 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛)))
10 simprr 771 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑋 = 𝑐)
116, 10sseqtrd 4007 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑆 𝑐)
12 unieq 4840 . . . . . . . . . . . 12 (𝑚 = 𝑐 𝑚 = 𝑐)
1312sseq2d 3999 . . . . . . . . . . 11 (𝑚 = 𝑐 → (𝑆 𝑚𝑆 𝑐))
14 pweq 4542 . . . . . . . . . . . . 13 (𝑚 = 𝑐 → 𝒫 𝑚 = 𝒫 𝑐)
1514ineq1d 4188 . . . . . . . . . . . 12 (𝑚 = 𝑐 → (𝒫 𝑚 ∩ Fin) = (𝒫 𝑐 ∩ Fin))
1615rexeqdv 3417 . . . . . . . . . . 11 (𝑚 = 𝑐 → (∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛 ↔ ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛))
1713, 16imbi12d 347 . . . . . . . . . 10 (𝑚 = 𝑐 → ((𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) ↔ (𝑆 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛)))
1817rspcv 3618 . . . . . . . . 9 (𝑐 ∈ 𝒫 𝐽 → (∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) → (𝑆 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛)))
1918ad2antrl 726 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) → (𝑆 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛)))
2011, 19mpid 44 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛))
219, 20sylbid 242 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑆) ∈ Comp → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛))
22 ssun2 4149 . . . . . . . . . 10 𝑇 ⊆ (𝑆𝑇)
23 sseq2 3993 . . . . . . . . . 10 (𝑋 = (𝑆𝑇) → (𝑇𝑋𝑇 ⊆ (𝑆𝑇)))
2422, 23mpbiri 260 . . . . . . . . 9 (𝑋 = (𝑆𝑇) → 𝑇𝑋)
2524ad2antlr 725 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑇𝑋)
267cmpsub 22002 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑇𝑋) → ((𝐽t 𝑇) ∈ Comp ↔ ∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠)))
272, 25, 26syl2anc 586 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑇) ∈ Comp ↔ ∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠)))
2825, 10sseqtrd 4007 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑇 𝑐)
29 unieq 4840 . . . . . . . . . . . 12 (𝑟 = 𝑐 𝑟 = 𝑐)
3029sseq2d 3999 . . . . . . . . . . 11 (𝑟 = 𝑐 → (𝑇 𝑟𝑇 𝑐))
31 pweq 4542 . . . . . . . . . . . . 13 (𝑟 = 𝑐 → 𝒫 𝑟 = 𝒫 𝑐)
3231ineq1d 4188 . . . . . . . . . . . 12 (𝑟 = 𝑐 → (𝒫 𝑟 ∩ Fin) = (𝒫 𝑐 ∩ Fin))
3332rexeqdv 3417 . . . . . . . . . . 11 (𝑟 = 𝑐 → (∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠 ↔ ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
3430, 33imbi12d 347 . . . . . . . . . 10 (𝑟 = 𝑐 → ((𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) ↔ (𝑇 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠)))
3534rspcv 3618 . . . . . . . . 9 (𝑐 ∈ 𝒫 𝐽 → (∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) → (𝑇 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠)))
3635ad2antrl 726 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) → (𝑇 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠)))
3728, 36mpid 44 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
3827, 37sylbid 242 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑇) ∈ Comp → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
39 reeanv 3368 . . . . . . 7 (∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)(𝑆 𝑛𝑇 𝑠) ↔ (∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
40 elinel1 4172 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛 ∈ 𝒫 𝑐)
4140elpwid 4553 . . . . . . . . . . . . . . 15 (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛𝑐)
42 elinel1 4172 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠 ∈ 𝒫 𝑐)
4342elpwid 4553 . . . . . . . . . . . . . . 15 (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠𝑐)
4441, 43anim12i 614 . . . . . . . . . . . . . 14 ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → (𝑛𝑐𝑠𝑐))
4544ad2antrl 726 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑐𝑠𝑐))
46 unss 4160 . . . . . . . . . . . . 13 ((𝑛𝑐𝑠𝑐) ↔ (𝑛𝑠) ⊆ 𝑐)
4745, 46sylib 220 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ⊆ 𝑐)
48 elinel2 4173 . . . . . . . . . . . . . 14 (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛 ∈ Fin)
49 elinel2 4173 . . . . . . . . . . . . . 14 (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠 ∈ Fin)
50 unfi 8779 . . . . . . . . . . . . . 14 ((𝑛 ∈ Fin ∧ 𝑠 ∈ Fin) → (𝑛𝑠) ∈ Fin)
5148, 49, 50syl2an 597 . . . . . . . . . . . . 13 ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → (𝑛𝑠) ∈ Fin)
5251ad2antrl 726 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ∈ Fin)
5347, 52jca 514 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → ((𝑛𝑠) ⊆ 𝑐 ∧ (𝑛𝑠) ∈ Fin))
54 elin 4169 . . . . . . . . . . . 12 ((𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin) ↔ ((𝑛𝑠) ∈ 𝒫 𝑐 ∧ (𝑛𝑠) ∈ Fin))
55 vex 3498 . . . . . . . . . . . . . 14 𝑐 ∈ V
5655elpw2 5241 . . . . . . . . . . . . 13 ((𝑛𝑠) ∈ 𝒫 𝑐 ↔ (𝑛𝑠) ⊆ 𝑐)
5756anbi1i 625 . . . . . . . . . . . 12 (((𝑛𝑠) ∈ 𝒫 𝑐 ∧ (𝑛𝑠) ∈ Fin) ↔ ((𝑛𝑠) ⊆ 𝑐 ∧ (𝑛𝑠) ∈ Fin))
5854, 57bitr2i 278 . . . . . . . . . . 11 (((𝑛𝑠) ⊆ 𝑐 ∧ (𝑛𝑠) ∈ Fin) ↔ (𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin))
5953, 58sylib 220 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin))
60 simpllr 774 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 = (𝑆𝑇))
61 ssun3 4150 . . . . . . . . . . . . . . . 16 (𝑆 𝑛𝑆 ⊆ ( 𝑛 𝑠))
62 ssun4 4151 . . . . . . . . . . . . . . . 16 (𝑇 𝑠𝑇 ⊆ ( 𝑛 𝑠))
6361, 62anim12i 614 . . . . . . . . . . . . . . 15 ((𝑆 𝑛𝑇 𝑠) → (𝑆 ⊆ ( 𝑛 𝑠) ∧ 𝑇 ⊆ ( 𝑛 𝑠)))
6463ad2antll 727 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑆 ⊆ ( 𝑛 𝑠) ∧ 𝑇 ⊆ ( 𝑛 𝑠)))
65 unss 4160 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ( 𝑛 𝑠) ∧ 𝑇 ⊆ ( 𝑛 𝑠)) ↔ (𝑆𝑇) ⊆ ( 𝑛 𝑠))
6664, 65sylib 220 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑆𝑇) ⊆ ( 𝑛 𝑠))
6760, 66eqsstrd 4005 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 ⊆ ( 𝑛 𝑠))
68 uniun 4851 . . . . . . . . . . . 12 (𝑛𝑠) = ( 𝑛 𝑠)
6967, 68sseqtrrdi 4018 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 (𝑛𝑠))
70 elpwi 4551 . . . . . . . . . . . . . . 15 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
7170adantr 483 . . . . . . . . . . . . . 14 ((𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐) → 𝑐𝐽)
7271ad2antlr 725 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑐𝐽)
7347, 72sstrd 3977 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ⊆ 𝐽)
74 uniss 4853 . . . . . . . . . . . . 13 ((𝑛𝑠) ⊆ 𝐽 (𝑛𝑠) ⊆ 𝐽)
7574, 7sseqtrrdi 4018 . . . . . . . . . . . 12 ((𝑛𝑠) ⊆ 𝐽 (𝑛𝑠) ⊆ 𝑋)
7673, 75syl 17 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ⊆ 𝑋)
7769, 76eqssd 3984 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 = (𝑛𝑠))
78 unieq 4840 . . . . . . . . . . 11 (𝑑 = (𝑛𝑠) → 𝑑 = (𝑛𝑠))
7978rspceeqv 3638 . . . . . . . . . 10 (((𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = (𝑛𝑠)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
8059, 77, 79syl2anc 586 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
8180exp32 423 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → ((𝑆 𝑛𝑇 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
8281rexlimdvv 3293 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)(𝑆 𝑛𝑇 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8339, 82syl5bir 245 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8421, 38, 83syl2and 609 . . . . 5 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8584impancom 454 . . . 4 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → ((𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8685expd 418 . . 3 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
8786ralrimiv 3181 . 2 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
887iscmp 21990 . 2 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
891, 87, 88sylanbrc 585 1 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → 𝐽 ∈ Comp)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138  ∃wrex 3139   ∪ cun 3934   ∩ cin 3935   ⊆ wss 3936  𝒫 cpw 4539  ∪ cuni 4832  (class class class)co 7150  Fincfn 8503   ↾t crest 16688  Topctop 21495  Compccmp 21988 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8283  df-en 8504  df-dom 8505  df-fin 8507  df-fi 8869  df-rest 16690  df-topgen 16711  df-top 21496  df-topon 21513  df-bases 21548  df-cmp 21989 This theorem is referenced by:  fiuncmp  22006
 Copyright terms: Public domain W3C validator