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

Theorem uncmp 23426
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 767 . 2 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → 𝐽 ∈ Top)
2 simpll 767 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝐽 ∈ Top)
3 ssun1 4187 . . . . . . . . . 10 𝑆 ⊆ (𝑆𝑇)
4 sseq2 4021 . . . . . . . . . 10 (𝑋 = (𝑆𝑇) → (𝑆𝑋𝑆 ⊆ (𝑆𝑇)))
53, 4mpbiri 258 . . . . . . . . 9 (𝑋 = (𝑆𝑇) → 𝑆𝑋)
65ad2antlr 727 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑆𝑋)
7 uncmp.1 . . . . . . . . 9 𝑋 = 𝐽
87cmpsub 23423 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑆𝑋) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛)))
92, 6, 8syl2anc 584 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑆) ∈ Comp ↔ ∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛)))
10 simprr 773 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑋 = 𝑐)
116, 10sseqtrd 4035 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑆 𝑐)
12 unieq 4922 . . . . . . . . . . . 12 (𝑚 = 𝑐 𝑚 = 𝑐)
1312sseq2d 4027 . . . . . . . . . . 11 (𝑚 = 𝑐 → (𝑆 𝑚𝑆 𝑐))
14 pweq 4618 . . . . . . . . . . . . 13 (𝑚 = 𝑐 → 𝒫 𝑚 = 𝒫 𝑐)
1514ineq1d 4226 . . . . . . . . . . . 12 (𝑚 = 𝑐 → (𝒫 𝑚 ∩ Fin) = (𝒫 𝑐 ∩ Fin))
1615rexeqdv 3324 . . . . . . . . . . 11 (𝑚 = 𝑐 → (∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛 ↔ ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛))
1713, 16imbi12d 344 . . . . . . . . . 10 (𝑚 = 𝑐 → ((𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) ↔ (𝑆 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛)))
1817rspcv 3617 . . . . . . . . 9 (𝑐 ∈ 𝒫 𝐽 → (∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) → (𝑆 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛)))
1918ad2antrl 728 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) → (𝑆 𝑐 → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛)))
2011, 19mpid 44 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑚 ∈ 𝒫 𝐽(𝑆 𝑚 → ∃𝑛 ∈ (𝒫 𝑚 ∩ Fin)𝑆 𝑛) → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛))
219, 20sylbid 240 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑆) ∈ Comp → ∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛))
22 ssun2 4188 . . . . . . . . . 10 𝑇 ⊆ (𝑆𝑇)
23 sseq2 4021 . . . . . . . . . 10 (𝑋 = (𝑆𝑇) → (𝑇𝑋𝑇 ⊆ (𝑆𝑇)))
2422, 23mpbiri 258 . . . . . . . . 9 (𝑋 = (𝑆𝑇) → 𝑇𝑋)
2524ad2antlr 727 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑇𝑋)
267cmpsub 23423 . . . . . . . 8 ((𝐽 ∈ Top ∧ 𝑇𝑋) → ((𝐽t 𝑇) ∈ Comp ↔ ∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠)))
272, 25, 26syl2anc 584 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑇) ∈ Comp ↔ ∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠)))
2825, 10sseqtrd 4035 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → 𝑇 𝑐)
29 unieq 4922 . . . . . . . . . . . 12 (𝑟 = 𝑐 𝑟 = 𝑐)
3029sseq2d 4027 . . . . . . . . . . 11 (𝑟 = 𝑐 → (𝑇 𝑟𝑇 𝑐))
31 pweq 4618 . . . . . . . . . . . . 13 (𝑟 = 𝑐 → 𝒫 𝑟 = 𝒫 𝑐)
3231ineq1d 4226 . . . . . . . . . . . 12 (𝑟 = 𝑐 → (𝒫 𝑟 ∩ Fin) = (𝒫 𝑐 ∩ Fin))
3332rexeqdv 3324 . . . . . . . . . . 11 (𝑟 = 𝑐 → (∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠 ↔ ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
3430, 33imbi12d 344 . . . . . . . . . 10 (𝑟 = 𝑐 → ((𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) ↔ (𝑇 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠)))
3534rspcv 3617 . . . . . . . . 9 (𝑐 ∈ 𝒫 𝐽 → (∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) → (𝑇 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠)))
3635ad2antrl 728 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) → (𝑇 𝑐 → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠)))
3728, 36mpid 44 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∀𝑟 ∈ 𝒫 𝐽(𝑇 𝑟 → ∃𝑠 ∈ (𝒫 𝑟 ∩ Fin)𝑇 𝑠) → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
3827, 37sylbid 240 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝐽t 𝑇) ∈ Comp → ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
39 reeanv 3226 . . . . . . 7 (∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)(𝑆 𝑛𝑇 𝑠) ↔ (∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠))
40 elinel1 4210 . . . . . . . . . . . . . . . 16 (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛 ∈ 𝒫 𝑐)
4140elpwid 4613 . . . . . . . . . . . . . . 15 (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛𝑐)
42 elinel1 4210 . . . . . . . . . . . . . . . 16 (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠 ∈ 𝒫 𝑐)
4342elpwid 4613 . . . . . . . . . . . . . . 15 (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠𝑐)
4441, 43anim12i 613 . . . . . . . . . . . . . 14 ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → (𝑛𝑐𝑠𝑐))
4544ad2antrl 728 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑐𝑠𝑐))
46 unss 4199 . . . . . . . . . . . . 13 ((𝑛𝑐𝑠𝑐) ↔ (𝑛𝑠) ⊆ 𝑐)
4745, 46sylib 218 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ⊆ 𝑐)
48 elinel2 4211 . . . . . . . . . . . . . 14 (𝑛 ∈ (𝒫 𝑐 ∩ Fin) → 𝑛 ∈ Fin)
49 elinel2 4211 . . . . . . . . . . . . . 14 (𝑠 ∈ (𝒫 𝑐 ∩ Fin) → 𝑠 ∈ Fin)
50 unfi 9209 . . . . . . . . . . . . . 14 ((𝑛 ∈ Fin ∧ 𝑠 ∈ Fin) → (𝑛𝑠) ∈ Fin)
5148, 49, 50syl2an 596 . . . . . . . . . . . . 13 ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → (𝑛𝑠) ∈ Fin)
5251ad2antrl 728 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ∈ Fin)
5347, 52jca 511 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → ((𝑛𝑠) ⊆ 𝑐 ∧ (𝑛𝑠) ∈ Fin))
54 elin 3978 . . . . . . . . . . . 12 ((𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin) ↔ ((𝑛𝑠) ∈ 𝒫 𝑐 ∧ (𝑛𝑠) ∈ Fin))
55 vex 3481 . . . . . . . . . . . . . 14 𝑐 ∈ V
5655elpw2 5339 . . . . . . . . . . . . 13 ((𝑛𝑠) ∈ 𝒫 𝑐 ↔ (𝑛𝑠) ⊆ 𝑐)
5756anbi1i 624 . . . . . . . . . . . 12 (((𝑛𝑠) ∈ 𝒫 𝑐 ∧ (𝑛𝑠) ∈ Fin) ↔ ((𝑛𝑠) ⊆ 𝑐 ∧ (𝑛𝑠) ∈ Fin))
5854, 57bitr2i 276 . . . . . . . . . . 11 (((𝑛𝑠) ⊆ 𝑐 ∧ (𝑛𝑠) ∈ Fin) ↔ (𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin))
5953, 58sylib 218 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin))
60 simpllr 776 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 = (𝑆𝑇))
61 ssun3 4189 . . . . . . . . . . . . . . . 16 (𝑆 𝑛𝑆 ⊆ ( 𝑛 𝑠))
62 ssun4 4190 . . . . . . . . . . . . . . . 16 (𝑇 𝑠𝑇 ⊆ ( 𝑛 𝑠))
6361, 62anim12i 613 . . . . . . . . . . . . . . 15 ((𝑆 𝑛𝑇 𝑠) → (𝑆 ⊆ ( 𝑛 𝑠) ∧ 𝑇 ⊆ ( 𝑛 𝑠)))
6463ad2antll 729 . . . . . . . . . . . . . 14 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑆 ⊆ ( 𝑛 𝑠) ∧ 𝑇 ⊆ ( 𝑛 𝑠)))
65 unss 4199 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ( 𝑛 𝑠) ∧ 𝑇 ⊆ ( 𝑛 𝑠)) ↔ (𝑆𝑇) ⊆ ( 𝑛 𝑠))
6664, 65sylib 218 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑆𝑇) ⊆ ( 𝑛 𝑠))
6760, 66eqsstrd 4033 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 ⊆ ( 𝑛 𝑠))
68 uniun 4934 . . . . . . . . . . . 12 (𝑛𝑠) = ( 𝑛 𝑠)
6967, 68sseqtrrdi 4046 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 (𝑛𝑠))
70 elpwi 4611 . . . . . . . . . . . . . . 15 (𝑐 ∈ 𝒫 𝐽𝑐𝐽)
7170adantr 480 . . . . . . . . . . . . . 14 ((𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐) → 𝑐𝐽)
7271ad2antlr 727 . . . . . . . . . . . . 13 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑐𝐽)
7347, 72sstrd 4005 . . . . . . . . . . . 12 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ⊆ 𝐽)
74 uniss 4919 . . . . . . . . . . . . 13 ((𝑛𝑠) ⊆ 𝐽 (𝑛𝑠) ⊆ 𝐽)
7574, 7sseqtrrdi 4046 . . . . . . . . . . . 12 ((𝑛𝑠) ⊆ 𝐽 (𝑛𝑠) ⊆ 𝑋)
7673, 75syl 17 . . . . . . . . . . 11 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → (𝑛𝑠) ⊆ 𝑋)
7769, 76eqssd 4012 . . . . . . . . . 10 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → 𝑋 = (𝑛𝑠))
78 unieq 4922 . . . . . . . . . . 11 (𝑑 = (𝑛𝑠) → 𝑑 = (𝑛𝑠))
7978rspceeqv 3644 . . . . . . . . . 10 (((𝑛𝑠) ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑋 = (𝑛𝑠)) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
8059, 77, 79syl2anc 584 . . . . . . . . 9 ((((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) ∧ ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) ∧ (𝑆 𝑛𝑇 𝑠))) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)
8180exp32 420 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((𝑛 ∈ (𝒫 𝑐 ∩ Fin) ∧ 𝑠 ∈ (𝒫 𝑐 ∩ Fin)) → ((𝑆 𝑛𝑇 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
8281rexlimdvv 3209 . . . . . . 7 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)(𝑆 𝑛𝑇 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8339, 82biimtrrid 243 . . . . . 6 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → ((∃𝑛 ∈ (𝒫 𝑐 ∩ Fin)𝑆 𝑛 ∧ ∃𝑠 ∈ (𝒫 𝑐 ∩ Fin)𝑇 𝑠) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8421, 38, 83syl2and 608 . . . . 5 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ (𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐)) → (((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8584impancom 451 . . . 4 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → ((𝑐 ∈ 𝒫 𝐽𝑋 = 𝑐) → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
8685expd 415 . . 3 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → (𝑐 ∈ 𝒫 𝐽 → (𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
8786ralrimiv 3142 . 2 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑))
887iscmp 23411 . 2 (𝐽 ∈ Comp ↔ (𝐽 ∈ Top ∧ ∀𝑐 ∈ 𝒫 𝐽(𝑋 = 𝑐 → ∃𝑑 ∈ (𝒫 𝑐 ∩ Fin)𝑋 = 𝑑)))
891, 87, 88sylanbrc 583 1 (((𝐽 ∈ Top ∧ 𝑋 = (𝑆𝑇)) ∧ ((𝐽t 𝑆) ∈ Comp ∧ (𝐽t 𝑇) ∈ Comp)) → 𝐽 ∈ Comp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1536  wcel 2105  wral 3058  wrex 3067  cun 3960  cin 3961  wss 3962  𝒫 cpw 4604   cuni 4911  (class class class)co 7430  Fincfn 8983  t crest 17466  Topctop 22914  Compccmp 23409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-1o 8504  df-en 8984  df-dom 8985  df-fin 8987  df-fi 9448  df-rest 17468  df-topgen 17489  df-top 22915  df-topon 22932  df-bases 22968  df-cmp 23410
This theorem is referenced by:  fiuncmp  23427
  Copyright terms: Public domain W3C validator