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

Theorem 2ndcomap 22707
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 22490 . . . . . 6 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top)
31, 2syl 17 . . . . 5 (𝜑𝐾 ∈ Top)
43ad2antrr 723 . . . 4 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝐾 ∈ Top)
5 simplll 772 . . . . . . 7 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥𝑏) → 𝜑)
6 bastg 22214 . . . . . . . . . 10 (𝑏 ∈ TopBases → 𝑏 ⊆ (topGen‘𝑏))
76ad2antlr 724 . . . . . . . . 9 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ⊆ (topGen‘𝑏))
8 simprr 770 . . . . . . . . 9 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘𝑏) = 𝐽)
97, 8sseqtrd 3971 . . . . . . . 8 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏𝐽)
109sselda 3931 . . . . . . 7 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥𝑏) → 𝑥𝐽)
11 2ndcomap.7 . . . . . . 7 ((𝜑𝑥𝐽) → (𝐹𝑥) ∈ 𝐾)
125, 10, 11syl2anc 584 . . . . . 6 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥𝑏) → (𝐹𝑥) ∈ 𝐾)
1312fmpttd 7039 . . . . 5 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥𝑏 ↦ (𝐹𝑥)):𝑏𝐾)
1413frnd 6653 . . . 4 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ⊆ 𝐾)
15 elunii 4856 . . . . . . . . . . 11 ((𝑧𝑘𝑘𝐾) → 𝑧 𝐾)
16 2ndcomap.2 . . . . . . . . . . 11 𝑌 = 𝐾
1715, 16eleqtrrdi 2848 . . . . . . . . . 10 ((𝑧𝑘𝑘𝐾) → 𝑧𝑌)
1817ancoms 459 . . . . . . . . 9 ((𝑘𝐾𝑧𝑘) → 𝑧𝑌)
1918adantl 482 . . . . . . . 8 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → 𝑧𝑌)
20 2ndcomap.6 . . . . . . . . 9 (𝜑 → ran 𝐹 = 𝑌)
2120ad3antrrr 727 . . . . . . . 8 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → ran 𝐹 = 𝑌)
2219, 21eleqtrrd 2840 . . . . . . 7 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → 𝑧 ∈ ran 𝐹)
23 eqid 2736 . . . . . . . . . . 11 𝐽 = 𝐽
2423, 16cnf 22495 . . . . . . . . . 10 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹: 𝐽𝑌)
251, 24syl 17 . . . . . . . . 9 (𝜑𝐹: 𝐽𝑌)
2625ad3antrrr 727 . . . . . . . 8 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → 𝐹: 𝐽𝑌)
27 ffn 6645 . . . . . . . 8 (𝐹: 𝐽𝑌𝐹 Fn 𝐽)
28 fvelrnb 6880 . . . . . . . 8 (𝐹 Fn 𝐽 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑡 𝐽(𝐹𝑡) = 𝑧))
2926, 27, 283syl 18 . . . . . . 7 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑡 𝐽(𝐹𝑡) = 𝑧))
3022, 29mpbid 231 . . . . . 6 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → ∃𝑡 𝐽(𝐹𝑡) = 𝑧)
311ad3antrrr 727 . . . . . . . . . . 11 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝐹 ∈ (𝐽 Cn 𝐾))
32 simprll 776 . . . . . . . . . . 11 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝑘𝐾)
33 cnima 22514 . . . . . . . . . . 11 ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑘𝐾) → (𝐹𝑘) ∈ 𝐽)
3431, 32, 33syl2anc 584 . . . . . . . . . 10 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (𝐹𝑘) ∈ 𝐽)
358adantr 481 . . . . . . . . . 10 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (topGen‘𝑏) = 𝐽)
3634, 35eleqtrrd 2840 . . . . . . . . 9 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (𝐹𝑘) ∈ (topGen‘𝑏))
37 simprrl 778 . . . . . . . . . 10 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝑡 𝐽)
38 simprrr 779 . . . . . . . . . . 11 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (𝐹𝑡) = 𝑧)
39 simprlr 777 . . . . . . . . . . 11 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝑧𝑘)
4038, 39eqeltrd 2837 . . . . . . . . . 10 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (𝐹𝑡) ∈ 𝑘)
4126ffnd 6646 . . . . . . . . . . . 12 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → 𝐹 Fn 𝐽)
4241adantrr 714 . . . . . . . . . . 11 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝐹 Fn 𝐽)
43 elpreima 6985 . . . . . . . . . . 11 (𝐹 Fn 𝐽 → (𝑡 ∈ (𝐹𝑘) ↔ (𝑡 𝐽 ∧ (𝐹𝑡) ∈ 𝑘)))
4442, 43syl 17 . . . . . . . . . 10 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → (𝑡 ∈ (𝐹𝑘) ↔ (𝑡 𝐽 ∧ (𝐹𝑡) ∈ 𝑘)))
4537, 40, 44mpbir2and 710 . . . . . . . . 9 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → 𝑡 ∈ (𝐹𝑘))
46 tg2 22213 . . . . . . . . 9 (((𝐹𝑘) ∈ (topGen‘𝑏) ∧ 𝑡 ∈ (𝐹𝑘)) → ∃𝑚𝑏 (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))
4736, 45, 46syl2anc 584 . . . . . . . 8 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → ∃𝑚𝑏 (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))
48 simprl 768 . . . . . . . . . . 11 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝑚𝑏)
49 eqid 2736 . . . . . . . . . . 11 (𝐹𝑚) = (𝐹𝑚)
50 imaeq2 5989 . . . . . . . . . . . 12 (𝑥 = 𝑚 → (𝐹𝑥) = (𝐹𝑚))
5150rspceeqv 3584 . . . . . . . . . . 11 ((𝑚𝑏 ∧ (𝐹𝑚) = (𝐹𝑚)) → ∃𝑥𝑏 (𝐹𝑚) = (𝐹𝑥))
5248, 49, 51sylancl 586 . . . . . . . . . 10 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → ∃𝑥𝑏 (𝐹𝑚) = (𝐹𝑥))
5342adantr 481 . . . . . . . . . . . . . 14 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝐹 Fn 𝐽)
54 fnfun 6579 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐽 → Fun 𝐹)
5553, 54syl 17 . . . . . . . . . . . . 13 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → Fun 𝐹)
56 simprrr 779 . . . . . . . . . . . . 13 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝑚 ⊆ (𝐹𝑘))
57 funimass2 6561 . . . . . . . . . . . . 13 ((Fun 𝐹𝑚 ⊆ (𝐹𝑘)) → (𝐹𝑚) ⊆ 𝑘)
5855, 56, 57syl2anc 584 . . . . . . . . . . . 12 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝐹𝑚) ⊆ 𝑘)
59 vex 3445 . . . . . . . . . . . 12 𝑘 ∈ V
60 ssexg 5264 . . . . . . . . . . . 12 (((𝐹𝑚) ⊆ 𝑘𝑘 ∈ V) → (𝐹𝑚) ∈ V)
6158, 59, 60sylancl 586 . . . . . . . . . . 11 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝐹𝑚) ∈ V)
62 eqid 2736 . . . . . . . . . . . 12 (𝑥𝑏 ↦ (𝐹𝑥)) = (𝑥𝑏 ↦ (𝐹𝑥))
6362elrnmpt 5891 . . . . . . . . . . 11 ((𝐹𝑚) ∈ V → ((𝐹𝑚) ∈ ran (𝑥𝑏 ↦ (𝐹𝑥)) ↔ ∃𝑥𝑏 (𝐹𝑚) = (𝐹𝑥)))
6461, 63syl 17 . . . . . . . . . 10 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → ((𝐹𝑚) ∈ ran (𝑥𝑏 ↦ (𝐹𝑥)) ↔ ∃𝑥𝑏 (𝐹𝑚) = (𝐹𝑥)))
6552, 64mpbird 256 . . . . . . . . 9 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝐹𝑚) ∈ ran (𝑥𝑏 ↦ (𝐹𝑥)))
6638adantr 481 . . . . . . . . . 10 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝐹𝑡) = 𝑧)
67 simprrl 778 . . . . . . . . . . 11 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝑡𝑚)
68 cnvimass 6013 . . . . . . . . . . . . 13 (𝐹𝑘) ⊆ dom 𝐹
6956, 68sstrdi 3943 . . . . . . . . . . . 12 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝑚 ⊆ dom 𝐹)
70 funfvima2 7157 . . . . . . . . . . . 12 ((Fun 𝐹𝑚 ⊆ dom 𝐹) → (𝑡𝑚 → (𝐹𝑡) ∈ (𝐹𝑚)))
7155, 69, 70syl2anc 584 . . . . . . . . . . 11 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝑡𝑚 → (𝐹𝑡) ∈ (𝐹𝑚)))
7267, 71mpd 15 . . . . . . . . . 10 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → (𝐹𝑡) ∈ (𝐹𝑚))
7366, 72eqeltrrd 2838 . . . . . . . . 9 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → 𝑧 ∈ (𝐹𝑚))
74 eleq2 2825 . . . . . . . . . . 11 (𝑤 = (𝐹𝑚) → (𝑧𝑤𝑧 ∈ (𝐹𝑚)))
75 sseq1 3956 . . . . . . . . . . 11 (𝑤 = (𝐹𝑚) → (𝑤𝑘 ↔ (𝐹𝑚) ⊆ 𝑘))
7674, 75anbi12d 631 . . . . . . . . . 10 (𝑤 = (𝐹𝑚) → ((𝑧𝑤𝑤𝑘) ↔ (𝑧 ∈ (𝐹𝑚) ∧ (𝐹𝑚) ⊆ 𝑘)))
7776rspcev 3570 . . . . . . . . 9 (((𝐹𝑚) ∈ ran (𝑥𝑏 ↦ (𝐹𝑥)) ∧ (𝑧 ∈ (𝐹𝑚) ∧ (𝐹𝑚) ⊆ 𝑘)) → ∃𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
7865, 73, 58, 77syl12anc 834 . . . . . . . 8 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) ∧ (𝑚𝑏 ∧ (𝑡𝑚𝑚 ⊆ (𝐹𝑘)))) → ∃𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
7947, 78rexlimddv 3154 . . . . . . 7 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘𝐾𝑧𝑘) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧))) → ∃𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
8079anassrs 468 . . . . . 6 (((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) ∧ (𝑡 𝐽 ∧ (𝐹𝑡) = 𝑧)) → ∃𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
8130, 80rexlimddv 3154 . . . . 5 ((((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘𝐾𝑧𝑘)) → ∃𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
8281ralrimivva 3193 . . . 4 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ∀𝑘𝐾𝑧𝑘𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘))
83 basgen2 22237 . . . 4 ((𝐾 ∈ Top ∧ ran (𝑥𝑏 ↦ (𝐹𝑥)) ⊆ 𝐾 ∧ ∀𝑘𝐾𝑧𝑘𝑤 ∈ ran (𝑥𝑏 ↦ (𝐹𝑥))(𝑧𝑤𝑤𝑘)) → (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) = 𝐾)
844, 14, 82, 83syl3anc 1370 . . 3 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) = 𝐾)
8584, 4eqeltrd 2837 . . . . 5 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) ∈ Top)
86 tgclb 22218 . . . . 5 (ran (𝑥𝑏 ↦ (𝐹𝑥)) ∈ TopBases ↔ (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) ∈ Top)
8785, 86sylibr 233 . . . 4 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ∈ TopBases)
88 omelon 9495 . . . . . . 7 ω ∈ On
89 simprl 768 . . . . . . 7 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ≼ ω)
90 ondomen 9886 . . . . . . 7 ((ω ∈ On ∧ 𝑏 ≼ ω) → 𝑏 ∈ dom card)
9188, 89, 90sylancr 587 . . . . . 6 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ∈ dom card)
9213ffnd 6646 . . . . . . 7 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥𝑏 ↦ (𝐹𝑥)) Fn 𝑏)
93 dffn4 6739 . . . . . . 7 ((𝑥𝑏 ↦ (𝐹𝑥)) Fn 𝑏 ↔ (𝑥𝑏 ↦ (𝐹𝑥)):𝑏onto→ran (𝑥𝑏 ↦ (𝐹𝑥)))
9492, 93sylib 217 . . . . . 6 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥𝑏 ↦ (𝐹𝑥)):𝑏onto→ran (𝑥𝑏 ↦ (𝐹𝑥)))
95 fodomnum 9906 . . . . . 6 (𝑏 ∈ dom card → ((𝑥𝑏 ↦ (𝐹𝑥)):𝑏onto→ran (𝑥𝑏 ↦ (𝐹𝑥)) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ 𝑏))
9691, 94, 95sylc 65 . . . . 5 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ 𝑏)
97 domtr 8860 . . . . 5 ((ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ 𝑏𝑏 ≼ ω) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ ω)
9896, 89, 97syl2anc 584 . . . 4 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ ω)
99 2ndci 22697 . . . 4 ((ran (𝑥𝑏 ↦ (𝐹𝑥)) ∈ TopBases ∧ ran (𝑥𝑏 ↦ (𝐹𝑥)) ≼ ω) → (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) ∈ 2ndω)
10087, 98, 99syl2anc 584 . . 3 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥𝑏 ↦ (𝐹𝑥))) ∈ 2ndω)
10184, 100eqeltrrd 2838 . 2 (((𝜑𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝐾 ∈ 2ndω)
102 2ndcomap.3 . . 3 (𝜑𝐽 ∈ 2ndω)
103 is2ndc 22695 . . 3 (𝐽 ∈ 2ndω ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
104102, 103sylib 217 . 2 (𝜑 → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽))
105101, 104r19.29a 3155 1 (𝜑𝐾 ∈ 2ndω)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wral 3061  wrex 3070  Vcvv 3441  wss 3897   cuni 4851   class class class wbr 5089  cmpt 5172  ccnv 5613  dom cdm 5614  ran crn 5615  cima 5617  Oncon0 6296  Fun wfun 6467   Fn wfn 6468  wf 6469  ontowfo 6471  cfv 6473  (class class class)co 7329  ωcom 7772  cdom 8794  cardccrd 9784  topGenctg 17237  Topctop 22140  TopBasesctb 22193   Cn ccn 22473  2ndωc2ndc 22687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642  ax-inf2 9490
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-int 4894  df-iun 4940  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-se 5570  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6232  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-isom 6482  df-riota 7286  df-ov 7332  df-oprab 7333  df-mpo 7334  df-om 7773  df-1st 7891  df-2nd 7892  df-frecs 8159  df-wrecs 8190  df-recs 8264  df-er 8561  df-map 8680  df-en 8797  df-dom 8798  df-card 9788  df-acn 9791  df-topgen 17243  df-top 22141  df-topon 22158  df-bases 22194  df-cn 22476  df-2ndc 22689
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator