MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bwth Structured version   Visualization version   GIF version
Theorem bwth 22905
Description: The glorious Bolzano-Weierstrass theorem. The first general topology theorem ever proved. The first mention of this theorem can be found in a course by Weierstrass from 1865. In his course Weierstrass called it a lemma. He didn't know how famous this theorem would be. He used a Euclidean space instead of a general compact space. And he was not aware of the Heine-Borel property. But the concepts of neighborhood and limit point were already there although not precisely defined. Cantor was one of his students. He published and used the theorem in an article from 1872. The rest of the general topology followed from that. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) Revised by BL to significantly shorten the proof and avoid infinity, regularity, and choice. (Revised by Brendan Leahy, 26-Dec-2018.)
Hypothesis
Ref Expression
bwt2.1 𝑋 = βˆͺ 𝐽
Assertion
Ref Expression
bwth ((𝐽 ∈ Comp ∧ 𝐴 βŠ† 𝑋 ∧ Β¬ 𝐴 ∈ Fin) β†’ βˆƒπ‘₯ ∈ 𝑋 π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄))
Distinct variable groups:   π‘₯,𝐴   π‘₯,𝐽   π‘₯,𝑋
Proof of Theorem bwth
Dummy variables π‘œ 𝑏 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pm3.24 403 . . . . . . 7 Β¬ ((𝐴 ∩ 𝑏) ∈ Fin ∧ Β¬ (𝐴 ∩ 𝑏) ∈ Fin)
21a1i 11 . . . . . 6 (𝑏 ∈ 𝑧 β†’ Β¬ ((𝐴 ∩ 𝑏) ∈ Fin ∧ Β¬ (𝐴 ∩ 𝑏) ∈ Fin))
32nrex 3074 . . . . 5 Β¬ βˆƒπ‘ ∈ 𝑧 ((𝐴 ∩ 𝑏) ∈ Fin ∧ Β¬ (𝐴 ∩ 𝑏) ∈ Fin)
4 r19.29 3114 . . . . 5 ((βˆ€π‘ ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin) β†’ βˆƒπ‘ ∈ 𝑧 ((𝐴 ∩ 𝑏) ∈ Fin ∧ Β¬ (𝐴 ∩ 𝑏) ∈ Fin))
53, 4mto 196 . . . 4 Β¬ (βˆ€π‘ ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)
65a1i 11 . . 3 (𝑧 ∈ (𝒫 𝐽 ∩ Fin) β†’ Β¬ (βˆ€π‘ ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin))
76nrex 3074 . 2 Β¬ βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(βˆ€π‘ ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)
8 ralnex 3072 . . . . . 6 (βˆ€π‘₯ ∈ 𝑋 Β¬ π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄) ↔ Β¬ βˆƒπ‘₯ ∈ 𝑋 π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄))
9 cmptop 22890 . . . . . . 7 (𝐽 ∈ Comp β†’ 𝐽 ∈ Top)
10 bwt2.1 . . . . . . . . . . 11 𝑋 = βˆͺ 𝐽
1110islp3 22641 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐴 βŠ† 𝑋 ∧ π‘₯ ∈ 𝑋) β†’ (π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄) ↔ βˆ€π‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 β†’ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…)))
12113expa 1118 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝐴 βŠ† 𝑋) ∧ π‘₯ ∈ 𝑋) β†’ (π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄) ↔ βˆ€π‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 β†’ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…)))
1312notbid 317 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝐴 βŠ† 𝑋) ∧ π‘₯ ∈ 𝑋) β†’ (Β¬ π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄) ↔ Β¬ βˆ€π‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 β†’ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…)))
1413ralbidva 3175 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴 βŠ† 𝑋) β†’ (βˆ€π‘₯ ∈ 𝑋 Β¬ π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄) ↔ βˆ€π‘₯ ∈ 𝑋 Β¬ βˆ€π‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 β†’ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…)))
159, 14sylan 580 . . . . . 6 ((𝐽 ∈ Comp ∧ 𝐴 βŠ† 𝑋) β†’ (βˆ€π‘₯ ∈ 𝑋 Β¬ π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄) ↔ βˆ€π‘₯ ∈ 𝑋 Β¬ βˆ€π‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 β†’ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…)))
168, 15bitr3id 284 . . . . 5 ((𝐽 ∈ Comp ∧ 𝐴 βŠ† 𝑋) β†’ (Β¬ βˆƒπ‘₯ ∈ 𝑋 π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄) ↔ βˆ€π‘₯ ∈ 𝑋 Β¬ βˆ€π‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 β†’ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…)))
17 rexanali 3102 . . . . . . . . 9 (βˆƒπ‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 ∧ Β¬ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…) ↔ Β¬ βˆ€π‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 β†’ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…))
18 nne 2944 . . . . . . . . . . . 12 (Β¬ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ… ↔ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) = βˆ…)
19 vex 3478 . . . . . . . . . . . . 13 π‘₯ ∈ V
20 sneq 4637 . . . . . . . . . . . . . . . 16 (π‘œ = π‘₯ β†’ {π‘œ} = {π‘₯})
2120difeq2d 4121 . . . . . . . . . . . . . . 15 (π‘œ = π‘₯ β†’ (𝐴 βˆ– {π‘œ}) = (𝐴 βˆ– {π‘₯}))
2221ineq2d 4211 . . . . . . . . . . . . . 14 (π‘œ = π‘₯ β†’ (𝑏 ∩ (𝐴 βˆ– {π‘œ})) = (𝑏 ∩ (𝐴 βˆ– {π‘₯})))
2322eqeq1d 2734 . . . . . . . . . . . . 13 (π‘œ = π‘₯ β†’ ((𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ… ↔ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) = βˆ…))
2419, 23spcev 3596 . . . . . . . . . . . 12 ((𝑏 ∩ (𝐴 βˆ– {π‘₯})) = βˆ… β†’ βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…)
2518, 24sylbi 216 . . . . . . . . . . 11 (Β¬ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ… β†’ βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…)
2625anim2i 617 . . . . . . . . . 10 ((π‘₯ ∈ 𝑏 ∧ Β¬ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…) β†’ (π‘₯ ∈ 𝑏 ∧ βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…))
2726reximi 3084 . . . . . . . . 9 (βˆƒπ‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 ∧ Β¬ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…) β†’ βˆƒπ‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 ∧ βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…))
2817, 27sylbir 234 . . . . . . . 8 (Β¬ βˆ€π‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 β†’ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…) β†’ βˆƒπ‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 ∧ βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…))
2928ralimi 3083 . . . . . . 7 (βˆ€π‘₯ ∈ 𝑋 Β¬ βˆ€π‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 β†’ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…) β†’ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 ∧ βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…))
3010cmpcov2 22885 . . . . . . . 8 ((𝐽 ∈ Comp ∧ βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 ∧ βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…)) β†’ βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = βˆͺ 𝑧 ∧ βˆ€π‘ ∈ 𝑧 βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…))
3130ex 413 . . . . . . 7 (𝐽 ∈ Comp β†’ (βˆ€π‘₯ ∈ 𝑋 βˆƒπ‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 ∧ βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…) β†’ βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = βˆͺ 𝑧 ∧ βˆ€π‘ ∈ 𝑧 βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…)))
3229, 31syl5 34 . . . . . 6 (𝐽 ∈ Comp β†’ (βˆ€π‘₯ ∈ 𝑋 Β¬ βˆ€π‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 β†’ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…) β†’ βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = βˆͺ 𝑧 ∧ βˆ€π‘ ∈ 𝑧 βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…)))
3332adantr 481 . . . . 5 ((𝐽 ∈ Comp ∧ 𝐴 βŠ† 𝑋) β†’ (βˆ€π‘₯ ∈ 𝑋 Β¬ βˆ€π‘ ∈ 𝐽 (π‘₯ ∈ 𝑏 β†’ (𝑏 ∩ (𝐴 βˆ– {π‘₯})) β‰  βˆ…) β†’ βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = βˆͺ 𝑧 ∧ βˆ€π‘ ∈ 𝑧 βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…)))
3416, 33sylbid 239 . . . 4 ((𝐽 ∈ Comp ∧ 𝐴 βŠ† 𝑋) β†’ (Β¬ βˆƒπ‘₯ ∈ 𝑋 π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄) β†’ βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = βˆͺ 𝑧 ∧ βˆ€π‘ ∈ 𝑧 βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…)))
35343adant3 1132 . . 3 ((𝐽 ∈ Comp ∧ 𝐴 βŠ† 𝑋 ∧ Β¬ 𝐴 ∈ Fin) β†’ (Β¬ βˆƒπ‘₯ ∈ 𝑋 π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄) β†’ βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = βˆͺ 𝑧 ∧ βˆ€π‘ ∈ 𝑧 βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…)))
36 elinel2 4195 . . . . . . . 8 (𝑧 ∈ (𝒫 𝐽 ∩ Fin) β†’ 𝑧 ∈ Fin)
37 sseq2 4007 . . . . . . . . . . . 12 (𝑋 = βˆͺ 𝑧 β†’ (𝐴 βŠ† 𝑋 ↔ 𝐴 βŠ† βˆͺ 𝑧))
3837biimpac 479 . . . . . . . . . . 11 ((𝐴 βŠ† 𝑋 ∧ 𝑋 = βˆͺ 𝑧) β†’ 𝐴 βŠ† βˆͺ 𝑧)
39 infssuni 9339 . . . . . . . . . . . . 13 ((Β¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin ∧ 𝐴 βŠ† βˆͺ 𝑧) β†’ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)
40393expa 1118 . . . . . . . . . . . 12 (((Β¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin) ∧ 𝐴 βŠ† βˆͺ 𝑧) β†’ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)
4140ancoms 459 . . . . . . . . . . 11 ((𝐴 βŠ† βˆͺ 𝑧 ∧ (Β¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin)) β†’ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)
4238, 41sylan 580 . . . . . . . . . 10 (((𝐴 βŠ† 𝑋 ∧ 𝑋 = βˆͺ 𝑧) ∧ (Β¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin)) β†’ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)
4342an42s 659 . . . . . . . . 9 (((𝐴 βŠ† 𝑋 ∧ Β¬ 𝐴 ∈ Fin) ∧ (𝑧 ∈ Fin ∧ 𝑋 = βˆͺ 𝑧)) β†’ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)
4443anassrs 468 . . . . . . . 8 ((((𝐴 βŠ† 𝑋 ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ Fin) ∧ 𝑋 = βˆͺ 𝑧) β†’ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)
4536, 44sylanl2 679 . . . . . . 7 ((((𝐴 βŠ† 𝑋 ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) ∧ 𝑋 = βˆͺ 𝑧) β†’ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)
46 0fin 9167 . . . . . . . . . . . 12 βˆ… ∈ Fin
47 eleq1 2821 . . . . . . . . . . . 12 ((𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ… β†’ ((𝑏 ∩ (𝐴 βˆ– {π‘œ})) ∈ Fin ↔ βˆ… ∈ Fin))
4846, 47mpbiri 257 . . . . . . . . . . 11 ((𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ… β†’ (𝑏 ∩ (𝐴 βˆ– {π‘œ})) ∈ Fin)
49 snfi 9040 . . . . . . . . . . 11 {π‘œ} ∈ Fin
50 unfi 9168 . . . . . . . . . . 11 (((𝑏 ∩ (𝐴 βˆ– {π‘œ})) ∈ Fin ∧ {π‘œ} ∈ Fin) β†’ ((𝑏 ∩ (𝐴 βˆ– {π‘œ})) βˆͺ {π‘œ}) ∈ Fin)
5148, 49, 50sylancl 586 . . . . . . . . . 10 ((𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ… β†’ ((𝑏 ∩ (𝐴 βˆ– {π‘œ})) βˆͺ {π‘œ}) ∈ Fin)
52 ssun1 4171 . . . . . . . . . . . 12 𝑏 βŠ† (𝑏 βˆͺ {π‘œ})
53 ssun1 4171 . . . . . . . . . . . . 13 𝐴 βŠ† (𝐴 βˆͺ {π‘œ})
54 undif1 4474 . . . . . . . . . . . . 13 ((𝐴 βˆ– {π‘œ}) βˆͺ {π‘œ}) = (𝐴 βˆͺ {π‘œ})
5553, 54sseqtrri 4018 . . . . . . . . . . . 12 𝐴 βŠ† ((𝐴 βˆ– {π‘œ}) βˆͺ {π‘œ})
56 ss2in 4235 . . . . . . . . . . . 12 ((𝑏 βŠ† (𝑏 βˆͺ {π‘œ}) ∧ 𝐴 βŠ† ((𝐴 βˆ– {π‘œ}) βˆͺ {π‘œ})) β†’ (𝑏 ∩ 𝐴) βŠ† ((𝑏 βˆͺ {π‘œ}) ∩ ((𝐴 βˆ– {π‘œ}) βˆͺ {π‘œ})))
5752, 55, 56mp2an 690 . . . . . . . . . . 11 (𝑏 ∩ 𝐴) βŠ† ((𝑏 βˆͺ {π‘œ}) ∩ ((𝐴 βˆ– {π‘œ}) βˆͺ {π‘œ}))
58 incom 4200 . . . . . . . . . . 11 (𝐴 ∩ 𝑏) = (𝑏 ∩ 𝐴)
59 undir 4275 . . . . . . . . . . 11 ((𝑏 ∩ (𝐴 βˆ– {π‘œ})) βˆͺ {π‘œ}) = ((𝑏 βˆͺ {π‘œ}) ∩ ((𝐴 βˆ– {π‘œ}) βˆͺ {π‘œ}))
6057, 58, 593sstr4i 4024 . . . . . . . . . 10 (𝐴 ∩ 𝑏) βŠ† ((𝑏 ∩ (𝐴 βˆ– {π‘œ})) βˆͺ {π‘œ})
61 ssfi 9169 . . . . . . . . . 10 ((((𝑏 ∩ (𝐴 βˆ– {π‘œ})) βˆͺ {π‘œ}) ∈ Fin ∧ (𝐴 ∩ 𝑏) βŠ† ((𝑏 ∩ (𝐴 βˆ– {π‘œ})) βˆͺ {π‘œ})) β†’ (𝐴 ∩ 𝑏) ∈ Fin)
6251, 60, 61sylancl 586 . . . . . . . . 9 ((𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ… β†’ (𝐴 ∩ 𝑏) ∈ Fin)
6362exlimiv 1933 . . . . . . . 8 (βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ… β†’ (𝐴 ∩ 𝑏) ∈ Fin)
6463ralimi 3083 . . . . . . 7 (βˆ€π‘ ∈ 𝑧 βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ… β†’ βˆ€π‘ ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin)
6545, 64anim12ci 614 . . . . . 6 (((((𝐴 βŠ† 𝑋 ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) ∧ 𝑋 = βˆͺ 𝑧) ∧ βˆ€π‘ ∈ 𝑧 βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…) β†’ (βˆ€π‘ ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin))
6665expl 458 . . . . 5 (((𝐴 βŠ† 𝑋 ∧ Β¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) β†’ ((𝑋 = βˆͺ 𝑧 ∧ βˆ€π‘ ∈ 𝑧 βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…) β†’ (βˆ€π‘ ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)))
6766reximdva 3168 . . . 4 ((𝐴 βŠ† 𝑋 ∧ Β¬ 𝐴 ∈ Fin) β†’ (βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = βˆͺ 𝑧 ∧ βˆ€π‘ ∈ 𝑧 βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…) β†’ βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(βˆ€π‘ ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)))
68673adant1 1130 . . 3 ((𝐽 ∈ Comp ∧ 𝐴 βŠ† 𝑋 ∧ Β¬ 𝐴 ∈ Fin) β†’ (βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = βˆͺ 𝑧 ∧ βˆ€π‘ ∈ 𝑧 βˆƒπ‘œ(𝑏 ∩ (𝐴 βˆ– {π‘œ})) = βˆ…) β†’ βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(βˆ€π‘ ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)))
6935, 68syld 47 . 2 ((𝐽 ∈ Comp ∧ 𝐴 βŠ† 𝑋 ∧ Β¬ 𝐴 ∈ Fin) β†’ (Β¬ βˆƒπ‘₯ ∈ 𝑋 π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄) β†’ βˆƒπ‘§ ∈ (𝒫 𝐽 ∩ Fin)(βˆ€π‘ ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ βˆƒπ‘ ∈ 𝑧 Β¬ (𝐴 ∩ 𝑏) ∈ Fin)))
707, 69mt3i 149 1 ((𝐽 ∈ Comp ∧ 𝐴 βŠ† 𝑋 ∧ Β¬ 𝐴 ∈ Fin) β†’ βˆƒπ‘₯ ∈ 𝑋 π‘₯ ∈ ((limPtβ€˜π½)β€˜π΄))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907  β€˜cfv 6540  Fincfn 8935  Topctop 22386  limPtclp 22629  Compccmp 22881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-iin 4999  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-om 7852  df-1o 8462  df-en 8936  df-fin 8939  df-top 22387  df-cld 22514  df-ntr 22515  df-cls 22516  df-lp 22631  df-cmp 22882
This theorem is referenced by:  poimirlem30  36506  fourierdlem42  44851
  Copyright terms: Public domain W3C validator