Step | Hyp | Ref
| Expression |
1 | | 2ndcomap.5 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
2 | | cntop2 20855 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐾 ∈ Top) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ Top) |
4 | 3 | ad2antrr 758 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝐾 ∈ Top) |
5 | | simplll 794 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥 ∈ 𝑏) → 𝜑) |
6 | | bastg 20581 |
. . . . . . . . . 10
⊢ (𝑏 ∈ TopBases → 𝑏 ⊆ (topGen‘𝑏)) |
7 | 6 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ⊆ (topGen‘𝑏)) |
8 | | simprr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘𝑏) = 𝐽) |
9 | 7, 8 | sseqtrd 3604 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ⊆ 𝐽) |
10 | 9 | sselda 3568 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥 ∈ 𝑏) → 𝑥 ∈ 𝐽) |
11 | | 2ndcomap.7 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾) |
12 | 5, 10, 11 | syl2anc 691 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ 𝑥 ∈ 𝑏) → (𝐹 “ 𝑥) ∈ 𝐾) |
13 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) = (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) |
14 | 12, 13 | fmptd 6292 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏⟶𝐾) |
15 | | frn 5966 |
. . . . 5
⊢ ((𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏⟶𝐾 → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ⊆ 𝐾) |
16 | 14, 15 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ⊆ 𝐾) |
17 | | elunii 4377 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑘 ∧ 𝑘 ∈ 𝐾) → 𝑧 ∈ ∪ 𝐾) |
18 | | 2ndcomap.2 |
. . . . . . . . . . 11
⊢ 𝑌 = ∪
𝐾 |
19 | 17, 18 | syl6eleqr 2699 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ 𝑘 ∧ 𝑘 ∈ 𝐾) → 𝑧 ∈ 𝑌) |
20 | 19 | ancoms 468 |
. . . . . . . . 9
⊢ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) → 𝑧 ∈ 𝑌) |
21 | 20 | adantl 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝑧 ∈ 𝑌) |
22 | | 2ndcomap.6 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 = 𝑌) |
23 | 22 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → ran 𝐹 = 𝑌) |
24 | 21, 23 | eleqtrrd 2691 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝑧 ∈ ran 𝐹) |
25 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝐽 =
∪ 𝐽 |
26 | 25, 18 | cnf 20860 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶𝑌) |
27 | 1, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:∪ 𝐽⟶𝑌) |
28 | 27 | ad3antrrr 762 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝐹:∪ 𝐽⟶𝑌) |
29 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:∪
𝐽⟶𝑌 → 𝐹 Fn ∪ 𝐽) |
30 | | fvelrnb 6153 |
. . . . . . . 8
⊢ (𝐹 Fn ∪
𝐽 → (𝑧 ∈ ran 𝐹 ↔ ∃𝑡 ∈ ∪ 𝐽(𝐹‘𝑡) = 𝑧)) |
31 | 28, 29, 30 | 3syl 18 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → (𝑧 ∈ ran 𝐹 ↔ ∃𝑡 ∈ ∪ 𝐽(𝐹‘𝑡) = 𝑧)) |
32 | 24, 31 | mpbid 221 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → ∃𝑡 ∈ ∪ 𝐽(𝐹‘𝑡) = 𝑧) |
33 | 1 | ad3antrrr 762 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝐹 ∈ (𝐽 Cn 𝐾)) |
34 | | simprll 798 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑘 ∈ 𝐾) |
35 | | cnima 20879 |
. . . . . . . . . . 11
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝑘 ∈ 𝐾) → (◡𝐹 “ 𝑘) ∈ 𝐽) |
36 | 33, 34, 35 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (◡𝐹 “ 𝑘) ∈ 𝐽) |
37 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (topGen‘𝑏) = 𝐽) |
38 | 36, 37 | eleqtrrd 2691 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (◡𝐹 “ 𝑘) ∈ (topGen‘𝑏)) |
39 | | simprrl 800 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑡 ∈ ∪ 𝐽) |
40 | | simprrr 801 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (𝐹‘𝑡) = 𝑧) |
41 | | simprlr 799 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑧 ∈ 𝑘) |
42 | 40, 41 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (𝐹‘𝑡) ∈ 𝑘) |
43 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → 𝐹 Fn ∪ 𝐽) |
44 | 43 | adantrr 749 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝐹 Fn ∪ 𝐽) |
45 | | elpreima 6245 |
. . . . . . . . . . 11
⊢ (𝐹 Fn ∪
𝐽 → (𝑡 ∈ (◡𝐹 “ 𝑘) ↔ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) ∈ 𝑘))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → (𝑡 ∈ (◡𝐹 “ 𝑘) ↔ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) ∈ 𝑘))) |
47 | 39, 42, 46 | mpbir2and 959 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → 𝑡 ∈ (◡𝐹 “ 𝑘)) |
48 | | tg2 20580 |
. . . . . . . . 9
⊢ (((◡𝐹 “ 𝑘) ∈ (topGen‘𝑏) ∧ 𝑡 ∈ (◡𝐹 “ 𝑘)) → ∃𝑚 ∈ 𝑏 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘))) |
49 | 38, 47, 48 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → ∃𝑚 ∈ 𝑏 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘))) |
50 | | simprl 790 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → 𝑚 ∈ 𝑏) |
51 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝐹 “ 𝑚) = (𝐹 “ 𝑚) |
52 | | imaeq2 5381 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑚 → (𝐹 “ 𝑥) = (𝐹 “ 𝑚)) |
53 | 52 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑚 → ((𝐹 “ 𝑚) = (𝐹 “ 𝑥) ↔ (𝐹 “ 𝑚) = (𝐹 “ 𝑚))) |
54 | 53 | rspcev 3282 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ 𝑏 ∧ (𝐹 “ 𝑚) = (𝐹 “ 𝑚)) → ∃𝑥 ∈ 𝑏 (𝐹 “ 𝑚) = (𝐹 “ 𝑥)) |
55 | 50, 51, 54 | sylancl 693 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → ∃𝑥 ∈ 𝑏 (𝐹 “ 𝑚) = (𝐹 “ 𝑥)) |
56 | 44 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → 𝐹 Fn ∪ 𝐽) |
57 | | fnfun 5902 |
. . . . . . . . . . . . . 14
⊢ (𝐹 Fn ∪
𝐽 → Fun 𝐹) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → Fun 𝐹) |
59 | | simprrr 801 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → 𝑚 ⊆ (◡𝐹 “ 𝑘)) |
60 | | funimass2 5886 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)) → (𝐹 “ 𝑚) ⊆ 𝑘) |
61 | 58, 59, 60 | syl2anc 691 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → (𝐹 “ 𝑚) ⊆ 𝑘) |
62 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑘 ∈ V |
63 | | ssexg 4732 |
. . . . . . . . . . . 12
⊢ (((𝐹 “ 𝑚) ⊆ 𝑘 ∧ 𝑘 ∈ V) → (𝐹 “ 𝑚) ∈ V) |
64 | 61, 62, 63 | sylancl 693 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → (𝐹 “ 𝑚) ∈ V) |
65 | 13 | elrnmpt 5293 |
. . . . . . . . . . 11
⊢ ((𝐹 “ 𝑚) ∈ V → ((𝐹 “ 𝑚) ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝑏 (𝐹 “ 𝑚) = (𝐹 “ 𝑥))) |
66 | 64, 65 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → ((𝐹 “ 𝑚) ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ↔ ∃𝑥 ∈ 𝑏 (𝐹 “ 𝑚) = (𝐹 “ 𝑥))) |
67 | 55, 66 | mpbird 246 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → (𝐹 “ 𝑚) ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) |
68 | 40 | adantr 480 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → (𝐹‘𝑡) = 𝑧) |
69 | | simprrl 800 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → 𝑡 ∈ 𝑚) |
70 | | cnvimass 5404 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 “ 𝑘) ⊆ dom 𝐹 |
71 | 59, 70 | syl6ss 3580 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → 𝑚 ⊆ dom 𝐹) |
72 | | funfvima2 6397 |
. . . . . . . . . . . 12
⊢ ((Fun
𝐹 ∧ 𝑚 ⊆ dom 𝐹) → (𝑡 ∈ 𝑚 → (𝐹‘𝑡) ∈ (𝐹 “ 𝑚))) |
73 | 58, 71, 72 | syl2anc 691 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → (𝑡 ∈ 𝑚 → (𝐹‘𝑡) ∈ (𝐹 “ 𝑚))) |
74 | 69, 73 | mpd 15 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → (𝐹‘𝑡) ∈ (𝐹 “ 𝑚)) |
75 | 68, 74 | eqeltrrd 2689 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → 𝑧 ∈ (𝐹 “ 𝑚)) |
76 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝐹 “ 𝑚) → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ (𝐹 “ 𝑚))) |
77 | | sseq1 3589 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝐹 “ 𝑚) → (𝑤 ⊆ 𝑘 ↔ (𝐹 “ 𝑚) ⊆ 𝑘)) |
78 | 76, 77 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑤 = (𝐹 “ 𝑚) → ((𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘) ↔ (𝑧 ∈ (𝐹 “ 𝑚) ∧ (𝐹 “ 𝑚) ⊆ 𝑘))) |
79 | 78 | rspcev 3282 |
. . . . . . . . 9
⊢ (((𝐹 “ 𝑚) ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∧ (𝑧 ∈ (𝐹 “ 𝑚) ∧ (𝐹 “ 𝑚) ⊆ 𝑘)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘)) |
80 | 67, 75, 61, 79 | syl12anc 1316 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) ∧ (𝑚 ∈ 𝑏 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ (◡𝐹 “ 𝑘)))) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘)) |
81 | 49, 80 | rexlimddv 3017 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ ((𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧))) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘)) |
82 | 81 | anassrs 678 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) ∧ (𝑡 ∈ ∪ 𝐽 ∧ (𝐹‘𝑡) = 𝑧)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘)) |
83 | 32, 82 | rexlimddv 3017 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) ∧ (𝑘 ∈ 𝐾 ∧ 𝑧 ∈ 𝑘)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘)) |
84 | 83 | ralrimivva 2954 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ∀𝑘 ∈ 𝐾 ∀𝑧 ∈ 𝑘 ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘)) |
85 | | basgen2 20604 |
. . . 4
⊢ ((𝐾 ∈ Top ∧ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ⊆ 𝐾 ∧ ∀𝑘 ∈ 𝐾 ∀𝑧 ∈ 𝑘 ∃𝑤 ∈ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑘)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) = 𝐾) |
86 | 4, 16, 84, 85 | syl3anc 1318 |
. . 3
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) = 𝐾) |
87 | 86, 4 | eqeltrd 2688 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈ Top) |
88 | | tgclb 20585 |
. . . . 5
⊢ (ran
(𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∈ TopBases ↔ (topGen‘ran
(𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈ Top) |
89 | 87, 88 | sylibr 223 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∈ TopBases) |
90 | | omelon 8426 |
. . . . . . 7
⊢ ω
∈ On |
91 | | simprl 790 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ≼ ω) |
92 | | ondomen 8743 |
. . . . . . 7
⊢ ((ω
∈ On ∧ 𝑏 ≼
ω) → 𝑏 ∈
dom card) |
93 | 90, 91, 92 | sylancr 694 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝑏 ∈ dom card) |
94 | | ffn 5958 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏⟶𝐾 → (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) Fn 𝑏) |
95 | 14, 94 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) Fn 𝑏) |
96 | | dffn4 6034 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) Fn 𝑏 ↔ (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏–onto→ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) |
97 | 95, 96 | sylib 207 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏–onto→ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) |
98 | | fodomnum 8763 |
. . . . . 6
⊢ (𝑏 ∈ dom card → ((𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)):𝑏–onto→ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ 𝑏)) |
99 | 93, 97, 98 | sylc 63 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ 𝑏) |
100 | | domtr 7895 |
. . . . 5
⊢ ((ran
(𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ 𝑏 ∧ 𝑏 ≼ ω) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ ω) |
101 | 99, 91, 100 | syl2anc 691 |
. . . 4
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ ω) |
102 | | 2ndci 21061 |
. . . 4
⊢ ((ran
(𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ∈ TopBases ∧ ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥)) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈
2nd𝜔) |
103 | 89, 101, 102 | syl2anc 691 |
. . 3
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → (topGen‘ran (𝑥 ∈ 𝑏 ↦ (𝐹 “ 𝑥))) ∈
2nd𝜔) |
104 | 86, 103 | eqeltrrd 2689 |
. 2
⊢ (((𝜑 ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) → 𝐾 ∈
2nd𝜔) |
105 | | 2ndcomap.3 |
. . 3
⊢ (𝜑 → 𝐽 ∈
2nd𝜔) |
106 | | is2ndc 21059 |
. . 3
⊢ (𝐽 ∈ 2nd𝜔
↔ ∃𝑏 ∈
TopBases (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝐽)) |
107 | 105, 106 | sylib 207 |
. 2
⊢ (𝜑 → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝐽)) |
108 | 104, 107 | r19.29a 3060 |
1
⊢ (𝜑 → 𝐾 ∈
2nd𝜔) |