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

Theorem uncmp 22770
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 766 . 2 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → 𝐽 ∈ Top)
2 simpll 766 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝐽 ∈ Top)
3 ssun1 4137 . . . . . . . . . 10 𝑆 ⊆ (𝑆𝑇)
4 sseq2 3975 . . . . . . . . . 10 (𝑋 = (𝑆𝑇) → (𝑆𝑋𝑆 ⊆ (𝑆𝑇)))
53, 4mpbiri 258 . . . . . . . . 9 (𝑋 = (𝑆𝑇) → 𝑆𝑋)
65ad2antlr 726 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑆𝑋)
7 uncmp.1 . . . . . . . . 9 𝑋 = 𝐽
87cmpsub 22767 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛)))
92, 6, 8syl2anc 585 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛)))
10 simprr 772 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑋 = 𝑐)
116, 10sseqtrd 3989 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑆 𝑐)
12 unieq 4881 . . . . . . . . . . . 12 (𝑚 = 𝑐 𝑚 = 𝑐)
1312sseq2d 3981 . . . . . . . . . . 11 (𝑚 = 𝑐 → (𝑆 𝑚𝑆 𝑐))
14 pweq 4579 . . . . . . . . . . . . 13 (𝑚 = 𝑐 → 𝒫 𝑚 = 𝒫 𝑐)
1514ineq1d 4176 . . . . . . . . . . . 12 (𝑚 = 𝑐 → (𝒫 𝑚 ∩ Fin) = (𝒫 𝑐 ∩ Fin))
1615rexeqdv 3317 . . . . . . . . . . 11 (𝑚 = 𝑐 → (∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛 ↔ ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛))
1713, 16imbi12d 345 . . . . . . . . . 10 (𝑚 = 𝑐 → ((𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) ↔ (𝑆 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛)))
1817rspcv 3580 . . . . . . . . 9 (𝑐 ∈ 𝒫 𝐽 → (∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) → (𝑆 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛)))
1918ad2antrl 727 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) → (𝑆 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛)))
2011, 19mpid 44 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛))
219, 20sylbid 239 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑆) ∈ Comp → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛))
22 ssun2 4138 . . . . . . . . . 10 𝑇 ⊆ (𝑆𝑇)
23 sseq2 3975 . . . . . . . . . 10 (𝑋 = (𝑆𝑇) → (𝑇𝑋𝑇 ⊆ (𝑆𝑇)))
2422, 23mpbiri 258 . . . . . . . . 9 (𝑋 = (𝑆𝑇) → 𝑇𝑋)
2524ad2antlr 726 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑇𝑋)
267cmpsub 22767 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑇𝑋) → ((𝐽t 𝑇) ∈ Comp ↔ ∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠)))
272, 25, 26syl2anc 585 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑇) ∈ Comp ↔ ∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠)))
2825, 10sseqtrd 3989 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑇 𝑐)
29 unieq 4881 . . . . . . . . . . . 12 (𝑟 = 𝑐 𝑟 = 𝑐)
3029sseq2d 3981 . . . . . . . . . . 11 (𝑟 = 𝑐 → (𝑇 𝑟𝑇 𝑐))
31 pweq 4579 . . . . . . . . . . . . 13 (𝑟 = 𝑐 → 𝒫 𝑟 = 𝒫 𝑐)
3231ineq1d 4176 . . . . . . . . . . . 12 (𝑟 = 𝑐 → (𝒫 𝑟 ∩ Fin) = (𝒫 𝑐 ∩ Fin))
3332rexeqdv 3317 . . . . . . . . . . 11 (𝑟 = 𝑐 → (∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠 ↔ ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
3430, 33imbi12d 345 . . . . . . . . . 10 (𝑟 = 𝑐 → ((𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) ↔ (𝑇 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠)))
3534rspcv 3580 . . . . . . . . 9 (𝑐 ∈ 𝒫 𝐽 → (∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) → (𝑇 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠)))
3635ad2antrl 727 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) → (𝑇 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠)))
3728, 36mpid 44 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
3827, 37sylbid 239 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑇) ∈ Comp → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
39 reeanv 3220 . . . . . . 7 (∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)(𝑆 𝑛𝑇 𝑠) ↔ (∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
40 elinel1 4160 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛 ∈ 𝒫 𝑐)
4140elpwid 4574 . . . . . . . . . . . . . . 15 (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛𝑐)
42 elinel1 4160 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠 ∈ 𝒫 𝑐)
4342elpwid 4574 . . . . . . . . . . . . . . 15 (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠𝑐)
4441, 43anim12i 614 . . . . . . . . . . . . . 14 ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → (𝑛𝑐𝑠𝑐))
4544ad2antrl 727 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑐𝑠𝑐))
46 unss 4149 . . . . . . . . . . . . 13 ((𝑛𝑐𝑠𝑐) ↔ (𝑛𝑠) ⊆ 𝑐)
4745, 46sylib 217 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ⊆ 𝑐)
48 elinel2 4161 . . . . . . . . . . . . . 14 (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛 ∈ Fin)
49 elinel2 4161 . . . . . . . . . . . . . 14 (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠 ∈ Fin)
50 unfi 9123 . . . . . . . . . . . . . 14 ((𝑛 ∈ Fin ∧ 𝑠 ∈ Fin) → (𝑛𝑠) ∈ Fin)
5148, 49, 50syl2an 597 . . . . . . . . . . . . 13 ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → (𝑛𝑠) ∈ Fin)
5251ad2antrl 727 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ∈ Fin)
5347, 52jca 513 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → ((𝑛𝑠) ⊆ 𝑐 ∧ (𝑛𝑠) ∈ Fin))
54 elin 3931 . . . . . . . . . . . 12 ((𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin) ↔ ((𝑛𝑠) ∈ 𝒫 𝑐 ∧ (𝑛𝑠) ∈ Fin))
55 vex 3452 . . . . . . . . . . . . . 14 𝑐 ∈ V
5655elpw2 5307 . . . . . . . . . . . . 13 ((𝑛𝑠) ∈ 𝒫 𝑐 ↔ (𝑛𝑠) ⊆ 𝑐)
5756anbi1i 625 . . . . . . . . . . . 12 (((𝑛𝑠) ∈ 𝒫 𝑐 ∧ (𝑛𝑠) ∈ Fin) ↔ ((𝑛𝑠) ⊆ 𝑐 ∧ (𝑛𝑠) ∈ Fin))
5854, 57bitr2i 276 . . . . . . . . . . 11 (((𝑛𝑠) ⊆ 𝑐 ∧ (𝑛𝑠) ∈ Fin) ↔ (𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin))
5953, 58sylib 217 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin))
60 simpllr 775 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 = (𝑆𝑇))
61 ssun3 4139 . . . . . . . . . . . . . . . 16 (𝑆 𝑛𝑆 ⊆ ( 𝑛 𝑠))
62 ssun4 4140 . . . . . . . . . . . . . . . 16 (𝑇 𝑠𝑇 ⊆ ( 𝑛 𝑠))
6361, 62anim12i 614 . . . . . . . . . . . . . . 15 ((𝑆 𝑛𝑇 𝑠) → (𝑆 ⊆ ( 𝑛 𝑠) ∧ 𝑇 ⊆ ( 𝑛 𝑠)))
6463ad2antll 728 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑆 ⊆ ( 𝑛 𝑠) ∧ 𝑇 ⊆ ( 𝑛 𝑠)))
65 unss 4149 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ( 𝑛 𝑠) ∧ 𝑇 ⊆ ( 𝑛 𝑠)) ↔ (𝑆𝑇) ⊆ ( 𝑛 𝑠))
6664, 65sylib 217 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑆𝑇) ⊆ ( 𝑛 𝑠))
6760, 66eqsstrd 3987 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 ⊆ ( 𝑛 𝑠))
68 uniun 4896 . . . . . . . . . . . 12 (𝑛𝑠) = ( 𝑛 𝑠)
6967, 68sseqtrrdi 4000 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 (𝑛𝑠))
70 elpwi 4572 . . . . . . . . . . . . . . 15 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
7170adantr 482 . . . . . . . . . . . . . 14 ((𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐) → 𝑐𝐽)
7271ad2antlr 726 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑐𝐽)
7347, 72sstrd 3959 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ⊆ 𝐽)
74 uniss 4878 . . . . . . . . . . . . 13 ((𝑛𝑠) ⊆ 𝐽 (𝑛𝑠) ⊆ 𝐽)
7574, 7sseqtrrdi 4000 . . . . . . . . . . . 12 ((𝑛𝑠) ⊆ 𝐽 (𝑛𝑠) ⊆ 𝑋)
7673, 75syl 17 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ⊆ 𝑋)
7769, 76eqssd 3966 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 = (𝑛𝑠))
78 unieq 4881 . . . . . . . . . . 11 (𝑑 = (𝑛𝑠) → 𝑑 = (𝑛𝑠))
7978rspceeqv 3600 . . . . . . . . . 10 (((𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = (𝑛𝑠)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
8059, 77, 79syl2anc 585 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
8180exp32 422 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → ((𝑆 𝑛𝑇 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
8281rexlimdvv 3205 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)(𝑆 𝑛𝑇 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8339, 82biimtrrid 242 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8421, 38, 83syl2and 609 . . . . 5 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8584impancom 453 . . . 4 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → ((𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8685expd 417 . . 3 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
8786ralrimiv 3143 . 2 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
887iscmp 22755 . 2 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
891, 87, 88sylanbrc 584 1 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → 𝐽 ∈ Comp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3065  wrex 3074  cun 3913  cin 3914  wss 3915  𝒫 cpw 4565   cuni 4870  (class class class)co 7362  Fincfn 8890  t crest 17309  Topctop 22258  Compccmp 22753
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-oprab 7366  df-mpo 7367  df-om 7808  df-1st 7926  df-2nd 7927  df-1o 8417  df-er 8655  df-en 8891  df-dom 8892  df-fin 8894  df-fi 9354  df-rest 17311  df-topgen 17332  df-top 22259  df-topon 22276  df-bases 22312  df-cmp 22754
This theorem is referenced by:  fiuncmp  22771
  Copyright terms: Public domain W3C validator