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

Theorem 2ndcomap 22058
Description: A surjective continuous open map maps second-countable spaces to second-countable spaces. (Contributed by Mario Carneiro, 9-Apr-2015.)
Hypotheses
Ref Expression
2ndcomap.2 𝑌 = 𝐾
2ndcomap.3 (𝜑𝐽 ∈ 2ndω)
2ndcomap.5 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
2ndcomap.6 (𝜑 → ran 𝐹 = 𝑌)
2ndcomap.7 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ 𝐾)
Assertion
Ref Expression
2ndcomap (𝜑𝐾 ∈ 2ndω)
Distinct variable groups:   𝑥,𝐹   𝑥,𝐽   𝜑,𝑥   𝑥,𝐾
Allowed substitution hint:   𝑌(𝑥)

Proof of Theorem 2ndcomap
Dummy variables 𝑘 𝑚 𝑡 𝑤 𝑧 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 2ndcomap.5 . . . . . 6 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
2 cntop2 21841 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
31, 2syl 17 . . . . 5 (𝜑𝐾 ∈ Top)
43ad2antrr 724 . . . 4 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝐾 ∈ Top)
5 simplll 773 . . . . . . 7 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥𝑏) → 𝜑)
6 bastg 21566 . . . . . . . . . 10 (𝑏 ∈ TopBases → 𝑏 ⊆ (topGen‘𝑏))
76ad2antlr 725 . . . . . . . . 9 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ⊆ (topGen‘𝑏))
8 simprr 771 . . . . . . . . 9 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘𝑏) = 𝐽)
97, 8sseqtrd 4005 . . . . . . . 8 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏𝐽)
109sselda 3965 . . . . . . 7 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥𝑏) → 𝑥𝐽)
11 2ndcomap.7 . . . . . . 7 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ 𝐾)
125, 10, 11syl2anc 586 . . . . . 6 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥𝑏) → (𝐹𝑥) ∈ 𝐾)
1312fmpttd 6872 . . . . 5 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥𝑏 ↦ (𝐹𝑥)):𝑏𝐾)
1413frnd 6514 . . . 4 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ⊆ 𝐾)
15 elunii 4835 . . . . . . . . . . 11 ((𝑧𝑘𝑘𝐾) → 𝑧 𝐾)
16 2ndcomap.2 . . . . . . . . . . 11 𝑌 = 𝐾
1715, 16eleqtrrdi 2922 . . . . . . . . . 10 ((𝑧𝑘𝑘𝐾) → 𝑧𝑌)
1817ancoms 461 . . . . . . . . 9 ((𝑘𝐾𝑧𝑘) → 𝑧𝑌)
1918adantl 484 . . . . . . . 8 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → 𝑧𝑌)
20 2ndcomap.6 . . . . . . . . 9 (𝜑 → ran 𝐹 = 𝑌)
2120ad3antrrr 728 . . . . . . . 8 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → ran 𝐹 = 𝑌)
2219, 21eleqtrrd 2914 . . . . . . 7 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → 𝑧 ∈ ran 𝐹)
23 eqid 2819 . . . . . . . . . . 11 𝐽 = 𝐽
2423, 16cnf 21846 . . . . . . . . . 10 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽𝑌)
251, 24syl 17 . . . . . . . . 9 (𝜑𝐹: 𝐽𝑌)
2625ad3antrrr 728 . . . . . . . 8 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → 𝐹: 𝐽𝑌)
27 ffn 6507 . . . . . . . 8 (𝐹: 𝐽𝑌𝐹 Fn 𝐽)
28 fvelrnb 6719 . . . . . . . 8 (𝐹 Fn 𝐽 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑡 𝐽(𝐹𝑡) = 𝑧))
2926, 27, 283syl 18 . . . . . . 7 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑡 𝐽(𝐹𝑡) = 𝑧))
3022, 29mpbid 234 . . . . . 6 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → ∃𝑡 𝐽(𝐹𝑡) = 𝑧)
311ad3antrrr 728 . . . . . . . . . . 11 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝐹 ∈ (𝐽 Cn 𝐾))
32 simprll 777 . . . . . . . . . . 11 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝑘𝐾)
33 cnima 21865 . . . . . . . . . . 11 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑘𝐾) → (𝐹𝑘) ∈ 𝐽)
3431, 32, 33syl2anc 586 . . . . . . . . . 10 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (𝐹𝑘) ∈ 𝐽)
358adantr 483 . . . . . . . . . 10 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (topGen‘𝑏) = 𝐽)
3634, 35eleqtrrd 2914 . . . . . . . . 9 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (𝐹𝑘) ∈ (topGen‘𝑏))
37 simprrl 779 . . . . . . . . . 10 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝑡 𝐽)
38 simprrr 780 . . . . . . . . . . 11 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (𝐹𝑡) = 𝑧)
39 simprlr 778 . . . . . . . . . . 11 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝑧𝑘)
4038, 39eqeltrd 2911 . . . . . . . . . 10 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (𝐹𝑡) ∈ 𝑘)
4126ffnd 6508 . . . . . . . . . . . 12 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → 𝐹 Fn 𝐽)
4241adantrr 715 . . . . . . . . . . 11 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝐹 Fn 𝐽)
43 elpreima 6821 . . . . . . . . . . 11 (𝐹 Fn 𝐽 → (𝑡 ∈ (𝐹𝑘) ↔ (𝑡 𝐽 ∧ (𝐹𝑡) ∈ 𝑘)))
4442, 43syl 17 . . . . . . . . . 10 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (𝑡 ∈ (𝐹𝑘) ↔ (𝑡 𝐽 ∧ (𝐹𝑡) ∈ 𝑘)))
4537, 40, 44mpbir2and 711 . . . . . . . . 9 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝑡 ∈ (𝐹𝑘))
46 tg2 21565 . . . . . . . . 9 (((𝐹𝑘) ∈ (topGen‘𝑏) ∧ 𝑡 ∈ (𝐹𝑘)) → ∃𝑚𝑏 (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))
4736, 45, 46syl2anc 586 . . . . . . . 8 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → ∃𝑚𝑏 (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))
48 simprl 769 . . . . . . . . . . 11 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝑚𝑏)
49 eqid 2819 . . . . . . . . . . 11 (𝐹𝑚) = (𝐹𝑚)
50 imaeq2 5918 . . . . . . . . . . . 12 (𝑥 = 𝑚 → (𝐹𝑥) = (𝐹𝑚))
5150rspceeqv 3636 . . . . . . . . . . 11 ((𝑚𝑏 ∧ (𝐹𝑚) = (𝐹𝑚)) → ∃𝑥𝑏 (𝐹𝑚) = (𝐹𝑥))
5248, 49, 51sylancl 588 . . . . . . . . . 10 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → ∃𝑥𝑏 (𝐹𝑚) = (𝐹𝑥))
5342adantr 483 . . . . . . . . . . . . . 14 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝐹 Fn 𝐽)
54 fnfun 6446 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐽 → Fun 𝐹)
5553, 54syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → Fun 𝐹)
56 simprrr 780 . . . . . . . . . . . . 13 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝑚 ⊆ (𝐹𝑘))
57 funimass2 6430 . . . . . . . . . . . . 13 ((Fun 𝐹𝑚 ⊆ (𝐹𝑘)) → (𝐹𝑚) ⊆ 𝑘)
5855, 56, 57syl2anc 586 . . . . . . . . . . . 12 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝐹𝑚) ⊆ 𝑘)
59 vex 3496 . . . . . . . . . . . 12 𝑘 ∈ V
60 ssexg 5218 . . . . . . . . . . . 12 (((𝐹𝑚) ⊆ 𝑘𝑘 ∈ V) → (𝐹𝑚) ∈ V)
6158, 59, 60sylancl 588 . . . . . . . . . . 11 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝐹𝑚) ∈ V)
62 eqid 2819 . . . . . . . . . . . 12 (𝑥𝑏 ↦ (𝐹𝑥)) = (𝑥𝑏 ↦ (𝐹𝑥))
6362elrnmpt 5821 . . . . . . . . . . 11 ((𝐹𝑚) ∈ V → ((𝐹𝑚) ∈ ran (𝑥𝑏 ↦ (𝐹𝑥)) ↔ ∃𝑥𝑏 (𝐹𝑚) = (𝐹𝑥)))
6461, 63syl 17 . . . . . . . . . 10 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → ((𝐹𝑚) ∈ ran (𝑥𝑏 ↦ (𝐹𝑥)) ↔ ∃𝑥𝑏 (𝐹𝑚) = (𝐹𝑥)))
6552, 64mpbird 259 . . . . . . . . 9 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝐹𝑚) ∈ ran (𝑥𝑏 ↦ (𝐹𝑥)))
6638adantr 483 . . . . . . . . . 10 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝐹𝑡) = 𝑧)
67 simprrl 779 . . . . . . . . . . 11 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝑡𝑚)
68 cnvimass 5942 . . . . . . . . . . . . 13 (𝐹𝑘) ⊆ dom 𝐹
6956, 68sstrdi 3977 . . . . . . . . . . . 12 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝑚 ⊆ dom 𝐹)
70 funfvima2 6985 . . . . . . . . . . . 12 ((Fun 𝐹𝑚 ⊆ dom 𝐹) → (𝑡𝑚 → (𝐹𝑡) ∈ (𝐹𝑚)))
7155, 69, 70syl2anc 586 . . . . . . . . . . 11 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝑡𝑚 → (𝐹𝑡) ∈ (𝐹𝑚)))
7267, 71mpd 15 . . . . . . . . . 10 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝐹𝑡) ∈ (𝐹𝑚))
7366, 72eqeltrrd 2912 . . . . . . . . 9 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝑧 ∈ (𝐹𝑚))
74 eleq2 2899 . . . . . . . . . . 11 (𝑤 = (𝐹𝑚) → (𝑧𝑤𝑧 ∈ (𝐹𝑚)))
75 sseq1 3990 . . . . . . . . . . 11 (𝑤 = (𝐹𝑚) → (𝑤𝑘 ↔ (𝐹𝑚) ⊆ 𝑘))
7674, 75anbi12d 632 . . . . . . . . . 10 (𝑤 = (𝐹𝑚) → ((𝑧𝑤𝑤𝑘) ↔ (𝑧 ∈ (𝐹𝑚) ∧ (𝐹𝑚) ⊆ 𝑘)))
7776rspcev 3621 . . . . . . . . 9 (((𝐹𝑚) ∈ ran (𝑥𝑏 ↦ (𝐹𝑥)) ∧ (𝑧 ∈ (𝐹𝑚) ∧ (𝐹𝑚) ⊆ 𝑘)) → ∃𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
7865, 73, 58, 77syl12anc 834 . . . . . . . 8 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → ∃𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
7947, 78rexlimddv 3289 . . . . . . 7 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → ∃𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
8079anassrs 470 . . . . . 6 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧)) → ∃𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
8130, 80rexlimddv 3289 . . . . 5 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → ∃𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
8281ralrimivva 3189 . . . 4 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ∀𝑘𝐾𝑧𝑘𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
83 basgen2 21589 . . . 4 ((𝐾 ∈ Top ∧ ran (𝑥𝑏 ↦ (𝐹𝑥)) ⊆ 𝐾 ∧ ∀𝑘𝐾𝑧𝑘𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘)) → (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) = 𝐾)
844, 14, 82, 83syl3anc 1365 . . 3 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) = 𝐾)
8584, 4eqeltrd 2911 . . . . 5 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) ∈ Top)
86 tgclb 21570 . . . . 5 (ran (𝑥𝑏 ↦ (𝐹𝑥)) ∈ TopBases ↔ (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) ∈ Top)
8785, 86sylibr 236 . . . 4 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ∈ TopBases)
88 omelon 9101 . . . . . . 7 ω ∈ On
89 simprl 769 . . . . . . 7 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ≼ ω)
90 ondomen 9455 . . . . . . 7 ((ω ∈ On ∧ 𝑏 ≼ ω) → 𝑏 ∈ dom card)
9188, 89, 90sylancr 589 . . . . . 6 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ∈ dom card)
9213ffnd 6508 . . . . . . 7 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥𝑏 ↦ (𝐹𝑥)) Fn 𝑏)
93 dffn4 6589 . . . . . . 7 ((𝑥𝑏 ↦ (𝐹𝑥)) Fn 𝑏 ↔ (𝑥𝑏 ↦ (𝐹𝑥)):𝑏onto→ran (𝑥𝑏 ↦ (𝐹𝑥)))
9492, 93sylib 220 . . . . . 6 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥𝑏 ↦ (𝐹𝑥)):𝑏onto→ran (𝑥𝑏 ↦ (𝐹𝑥)))
95 fodomnum 9475 . . . . . 6 (𝑏 ∈ dom card → ((𝑥𝑏 ↦ (𝐹𝑥)):𝑏onto→ran (𝑥𝑏 ↦ (𝐹𝑥)) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ 𝑏))
9691, 94, 95sylc 65 . . . . 5 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ 𝑏)
97 domtr 8554 . . . . 5 ((ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ 𝑏𝑏 ≼ ω) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ ω)
9896, 89, 97syl2anc 586 . . . 4 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ ω)
99 2ndci 22048 . . . 4 ((ran (𝑥𝑏 ↦ (𝐹𝑥)) ∈ TopBases ∧ ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ ω) → (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) ∈ 2ndω)
10087, 98, 99syl2anc 586 . . 3 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) ∈ 2ndω)
10184, 100eqeltrrd 2912 . 2 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝐾 ∈ 2ndω)
102 2ndcomap.3 . . 3 (𝜑𝐽 ∈ 2ndω)
103 is2ndc 22046 . . 3 (𝐽 ∈ 2ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
104102, 103sylib 220 . 2 (𝜑 → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
105101, 104r19.29a 3287 1 (𝜑𝐾 ∈ 2ndω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1530  wcel 2107  wral 3136  wrex 3137  Vcvv 3493  wss 3934   cuni 4830   class class class wbr 5057  cmpt 5137  ccnv 5547  dom cdm 5548  ran crn 5549  cima 5551  Oncon0 6184  Fun wfun 6342   Fn wfn 6343  wf 6344  ontowfo 6346  cfv 6348  (class class class)co 7148  ωcom 7572  cdom 8499  cardccrd 9356  topGenctg 16703  Topctop 21493  TopBasesctb 21545   Cn ccn 21824  2ndωc2ndc 22038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-inf2 9096
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-er 8281  df-map 8400  df-en 8502  df-dom 8503  df-card 9360  df-acn 9363  df-topgen 16709  df-top 21494  df-topon 21511  df-bases 21546  df-cn 21827  df-2ndc 22040
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator