Step | Hyp | Ref
| Expression |
1 | | simpr 484 |
. . 3
⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
→ 𝐽 ∈
2ndω) |
2 | | is2ndc 23475 |
. . 3
⊢ (𝐽 ∈ 2ndω
↔ ∃𝑐 ∈
TopBases (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽)) |
3 | 1, 2 | sylib 218 |
. 2
⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
→ ∃𝑐 ∈
TopBases (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽)) |
4 | | vex 3492 |
. . . . . . 7
⊢ 𝑐 ∈ V |
5 | 4, 4 | xpex 7788 |
. . . . . 6
⊢ (𝑐 × 𝑐) ∈ V |
6 | | 3simpa 1148 |
. . . . . . . 8
⊢ ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) → (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)) |
7 | 6 | ssopab2i 5569 |
. . . . . . 7
⊢
{〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))} ⊆ {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)} |
8 | | 2ndcctbss.2 |
. . . . . . 7
⊢ 𝑆 = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣))} |
9 | | df-xp 5706 |
. . . . . . 7
⊢ (𝑐 × 𝑐) = {〈𝑢, 𝑣〉 ∣ (𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐)} |
10 | 7, 8, 9 | 3sstr4i 4052 |
. . . . . 6
⊢ 𝑆 ⊆ (𝑐 × 𝑐) |
11 | | ssdomg 9060 |
. . . . . 6
⊢ ((𝑐 × 𝑐) ∈ V → (𝑆 ⊆ (𝑐 × 𝑐) → 𝑆 ≼ (𝑐 × 𝑐))) |
12 | 5, 10, 11 | mp2 9 |
. . . . 5
⊢ 𝑆 ≼ (𝑐 × 𝑐) |
13 | 4 | xpdom1 9137 |
. . . . . . . . 9
⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ (ω × 𝑐)) |
14 | | omex 9712 |
. . . . . . . . . 10
⊢ ω
∈ V |
15 | 14 | xpdom2 9133 |
. . . . . . . . 9
⊢ (𝑐 ≼ ω → (ω
× 𝑐) ≼ (ω
× ω)) |
16 | | domtr 9067 |
. . . . . . . . 9
⊢ (((𝑐 × 𝑐) ≼ (ω × 𝑐) ∧ (ω × 𝑐) ≼ (ω × ω)) →
(𝑐 × 𝑐) ≼ (ω ×
ω)) |
17 | 13, 15, 16 | syl2anc 583 |
. . . . . . . 8
⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ (ω ×
ω)) |
18 | | xpomen 10084 |
. . . . . . . 8
⊢ (ω
× ω) ≈ ω |
19 | | domentr 9073 |
. . . . . . . 8
⊢ (((𝑐 × 𝑐) ≼ (ω × ω) ∧
(ω × ω) ≈ ω) → (𝑐 × 𝑐) ≼ ω) |
20 | 17, 18, 19 | sylancl 585 |
. . . . . . 7
⊢ (𝑐 ≼ ω → (𝑐 × 𝑐) ≼ ω) |
21 | 20 | adantr 480 |
. . . . . 6
⊢ ((𝑐 ≼ ω ∧
(topGen‘𝑐) = 𝐽) → (𝑐 × 𝑐) ≼ ω) |
22 | 21 | ad2antll 728 |
. . . . 5
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → (𝑐 × 𝑐) ≼ ω) |
23 | | domtr 9067 |
. . . . 5
⊢ ((𝑆 ≼ (𝑐 × 𝑐) ∧ (𝑐 × 𝑐) ≼ ω) → 𝑆 ≼ ω) |
24 | 12, 22, 23 | sylancr 586 |
. . . 4
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → 𝑆 ≼
ω) |
25 | 8 | relopabiv 5844 |
. . . . . . . . 9
⊢ Rel 𝑆 |
26 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
27 | | 1st2nd 8080 |
. . . . . . . . 9
⊢ ((Rel
𝑆 ∧ 𝑥 ∈ 𝑆) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
28 | 25, 26, 27 | sylancr 586 |
. . . . . . . 8
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
29 | 28, 26 | eqeltrrd 2845 |
. . . . . . 7
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑆) |
30 | | df-br 5167 |
. . . . . . . . 9
⊢
((1st ‘𝑥)𝑆(2nd ‘𝑥) ↔ 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑆) |
31 | | fvex 6933 |
. . . . . . . . . 10
⊢
(1st ‘𝑥) ∈ V |
32 | | fvex 6933 |
. . . . . . . . . 10
⊢
(2nd ‘𝑥) ∈ V |
33 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → 𝑢 = (1st ‘𝑥)) |
34 | 33 | eleq1d 2829 |
. . . . . . . . . . 11
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (𝑢 ∈ 𝑐 ↔ (1st ‘𝑥) ∈ 𝑐)) |
35 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → 𝑣 = (2nd ‘𝑥)) |
36 | 35 | eleq1d 2829 |
. . . . . . . . . . 11
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (𝑣 ∈ 𝑐 ↔ (2nd ‘𝑥) ∈ 𝑐)) |
37 | | sseq1 4034 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (1st ‘𝑥) → (𝑢 ⊆ 𝑤 ↔ (1st ‘𝑥) ⊆ 𝑤)) |
38 | | sseq2 4035 |
. . . . . . . . . . . . 13
⊢ (𝑣 = (2nd ‘𝑥) → (𝑤 ⊆ 𝑣 ↔ 𝑤 ⊆ (2nd ‘𝑥))) |
39 | 37, 38 | bi2anan9 637 |
. . . . . . . . . . . 12
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → ((𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))) |
40 | 39 | rexbidv 3185 |
. . . . . . . . . . 11
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → (∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))) |
41 | 34, 36, 40 | 3anbi123d 1436 |
. . . . . . . . . 10
⊢ ((𝑢 = (1st ‘𝑥) ∧ 𝑣 = (2nd ‘𝑥)) → ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))))) |
42 | 31, 32, 41, 8 | braba 5556 |
. . . . . . . . 9
⊢
((1st ‘𝑥)𝑆(2nd ‘𝑥) ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))) |
43 | 30, 42 | bitr3i 277 |
. . . . . . . 8
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑆 ↔ ((1st ‘𝑥) ∈ 𝑐 ∧ (2nd ‘𝑥) ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)))) |
44 | 43 | simp3bi 1147 |
. . . . . . 7
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ 𝑆 → ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) |
45 | 29, 44 | syl 17 |
. . . . . 6
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → ∃𝑤 ∈ 𝐵 ((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) |
46 | | fvi 6998 |
. . . . . . 7
⊢ (𝐵 ∈ TopBases → ( I
‘𝐵) = 𝐵) |
47 | 46 | ad3antrrr 729 |
. . . . . 6
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → ( I ‘𝐵) = 𝐵) |
48 | 45, 47 | rexeqtrrdv 3339 |
. . . . 5
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ 𝑥 ∈ 𝑆) → ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) |
49 | 48 | ralrimiva 3152 |
. . . 4
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ∀𝑥 ∈ 𝑆 ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) |
50 | | fvex 6933 |
. . . . 5
⊢ ( I
‘𝐵) ∈
V |
51 | | sseq2 4035 |
. . . . . 6
⊢ (𝑤 = (𝑓‘𝑥) → ((1st ‘𝑥) ⊆ 𝑤 ↔ (1st ‘𝑥) ⊆ (𝑓‘𝑥))) |
52 | | sseq1 4034 |
. . . . . 6
⊢ (𝑤 = (𝑓‘𝑥) → (𝑤 ⊆ (2nd ‘𝑥) ↔ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) |
53 | 51, 52 | anbi12d 631 |
. . . . 5
⊢ (𝑤 = (𝑓‘𝑥) → (((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥)) ↔ ((1st
‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) |
54 | 50, 53 | axcc4dom 10510 |
. . . 4
⊢ ((𝑆 ≼ ω ∧
∀𝑥 ∈ 𝑆 ∃𝑤 ∈ ( I ‘𝐵)((1st ‘𝑥) ⊆ 𝑤 ∧ 𝑤 ⊆ (2nd ‘𝑥))) → ∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) |
55 | 24, 49, 54 | syl2anc 583 |
. . 3
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) |
56 | 46 | ad2antrr 725 |
. . . . . . 7
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ( I
‘𝐵) = 𝐵) |
57 | 56 | feq3d 6734 |
. . . . . 6
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → (𝑓:𝑆⟶( I ‘𝐵) ↔ 𝑓:𝑆⟶𝐵)) |
58 | 57 | anbi1d 630 |
. . . . 5
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ((𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ↔ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))))) |
59 | | 2ndctop 23476 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ 2ndω
→ 𝐽 ∈
Top) |
60 | 59 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
→ 𝐽 ∈
Top) |
61 | 60 | ad2antrr 725 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐽 ∈ Top) |
62 | | frn 6754 |
. . . . . . . . . . . 12
⊢ (𝑓:𝑆⟶𝐵 → ran 𝑓 ⊆ 𝐵) |
63 | 62 | ad2antrl 727 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ⊆ 𝐵) |
64 | | bastg 22994 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ TopBases → 𝐵 ⊆ (topGen‘𝐵)) |
65 | 64 | ad3antrrr 729 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐵 ⊆ (topGen‘𝐵)) |
66 | | 2ndcctbss.1 |
. . . . . . . . . . . 12
⊢ 𝐽 = (topGen‘𝐵) |
67 | 65, 66 | sseqtrrdi 4060 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐵 ⊆ 𝐽) |
68 | 63, 67 | sstrd 4019 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ⊆ 𝐽) |
69 | | simprrl 780 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑜 ∈ 𝐽) |
70 | | simprr 772 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧
(topGen‘𝑐) = 𝐽)) → (topGen‘𝑐) = 𝐽) |
71 | 70 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → (topGen‘𝑐) = 𝐽) |
72 | 69, 71 | eleqtrrd 2847 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑜 ∈ (topGen‘𝑐)) |
73 | | simprrr 781 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝑡 ∈ 𝑜) |
74 | | tg2 22993 |
. . . . . . . . . . . . . 14
⊢ ((𝑜 ∈ (topGen‘𝑐) ∧ 𝑡 ∈ 𝑜) → ∃𝑑 ∈ 𝑐 (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) |
75 | 72, 73, 74 | syl2anc 583 |
. . . . . . . . . . . . 13
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ∃𝑑 ∈ 𝑐 (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) |
76 | | bastg 22994 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ∈ TopBases → 𝑐 ⊆ (topGen‘𝑐)) |
77 | 76 | ad2antrl 727 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → 𝑐 ⊆ (topGen‘𝑐)) |
78 | 77 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑐 ⊆ (topGen‘𝑐)) |
79 | 66 | eqeq2i 2753 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((topGen‘𝑐) =
𝐽 ↔
(topGen‘𝑐) =
(topGen‘𝐵)) |
80 | 79 | biimpi 216 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((topGen‘𝑐) =
𝐽 →
(topGen‘𝑐) =
(topGen‘𝐵)) |
81 | 80 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑐 ≼ ω ∧
(topGen‘𝑐) = 𝐽) → (topGen‘𝑐) = (topGen‘𝐵)) |
82 | 81 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) →
(topGen‘𝑐) =
(topGen‘𝐵)) |
83 | 82 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → (topGen‘𝑐) = (topGen‘𝐵)) |
84 | 78, 83 | sseqtrd 4049 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑐 ⊆ (topGen‘𝐵)) |
85 | | simprl 770 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑑 ∈ 𝑐) |
86 | 84, 85 | sseldd 4009 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑑 ∈ (topGen‘𝐵)) |
87 | | simprrl 780 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑡 ∈ 𝑑) |
88 | | tg2 22993 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ (topGen‘𝐵) ∧ 𝑡 ∈ 𝑑) → ∃𝑚 ∈ 𝐵 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) |
89 | 86, 87, 88 | syl2anc 583 |
. . . . . . . . . . . . . 14
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → ∃𝑚 ∈ 𝐵 (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) |
90 | 64 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → 𝐵 ⊆ (topGen‘𝐵)) |
91 | 90 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝐵 ⊆ (topGen‘𝐵)) |
92 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → (topGen‘𝑐) = 𝐽) |
93 | 92, 66 | eqtr2di 2797 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → (topGen‘𝐵) = (topGen‘𝑐)) |
94 | 91, 93 | sseqtrd 4049 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝐵 ⊆ (topGen‘𝑐)) |
95 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑚 ∈ 𝐵) |
96 | 94, 95 | sseldd 4009 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑚 ∈ (topGen‘𝑐)) |
97 | | simprrl 780 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑡 ∈ 𝑚) |
98 | | tg2 22993 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ (topGen‘𝑐) ∧ 𝑡 ∈ 𝑚) → ∃𝑛 ∈ 𝑐 (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) |
99 | 96, 97, 98 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → ∃𝑛 ∈ 𝑐 (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) |
100 | | ffn 6747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓:𝑆⟶𝐵 → 𝑓 Fn 𝑆) |
101 | 100 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜)) → 𝑓 Fn 𝑆) |
102 | 101 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → 𝑓 Fn 𝑆) |
103 | 102 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑓 Fn 𝑆) |
104 | | simprl 770 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ∈ 𝑐) |
105 | 85 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑑 ∈ 𝑐) |
106 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ∈ 𝐵) |
107 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ⊆ 𝑚) |
108 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → 𝑚 ⊆ 𝑑) |
109 | 108 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ⊆ 𝑑) |
110 | | sseq2 4035 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑚 → (𝑛 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑚)) |
111 | | sseq1 4034 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = 𝑚 → (𝑤 ⊆ 𝑑 ↔ 𝑚 ⊆ 𝑑)) |
112 | 110, 111 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑚 → ((𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑) ↔ (𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑))) |
113 | 112 | rspcev 3635 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ 𝐵 ∧ (𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)) |
114 | 106, 107,
109, 113 | syl12anc 836 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)) |
115 | | df-br 5167 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛𝑆𝑑 ↔ 〈𝑛, 𝑑〉 ∈ 𝑆) |
116 | | vex 3492 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑛 ∈ V |
117 | | vex 3492 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑑 ∈ V |
118 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → 𝑢 = 𝑛) |
119 | 118 | eleq1d 2829 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (𝑢 ∈ 𝑐 ↔ 𝑛 ∈ 𝑐)) |
120 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → 𝑣 = 𝑑) |
121 | 120 | eleq1d 2829 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (𝑣 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐)) |
122 | | sseq1 4034 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑢 = 𝑛 → (𝑢 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑤)) |
123 | | sseq2 4035 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 = 𝑑 → (𝑤 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑑)) |
124 | 122, 123 | bi2anan9 637 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → ((𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))) |
125 | 124 | rexbidv 3185 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → (∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣) ↔ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))) |
126 | 119, 121,
125 | 3anbi123d 1436 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑢 = 𝑛 ∧ 𝑣 = 𝑑) → ((𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣)) ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)))) |
127 | 116, 117,
126, 8 | braba 5556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛𝑆𝑑 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))) |
128 | 115, 127 | bitr3i 277 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑛, 𝑑〉 ∈ 𝑆 ↔ (𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑))) |
129 | 104, 105,
114, 128 | syl3anbrc 1343 |
. . . . . . . . . . . . . . . . 17
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 〈𝑛, 𝑑〉 ∈ 𝑆) |
130 | | fnfvelrn 7114 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑓 Fn 𝑆 ∧ 〈𝑛, 𝑑〉 ∈ 𝑆) → (𝑓‘〈𝑛, 𝑑〉) ∈ ran 𝑓) |
131 | 103, 129,
130 | syl2anc 583 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑓‘〈𝑛, 𝑑〉) ∈ ran 𝑓) |
132 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ∈ 𝑐) |
133 | | simplll 774 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑑 ∈ 𝑐) |
134 | | simplrl 776 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ∈ 𝐵) |
135 | | simprrr 781 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑛 ⊆ 𝑚) |
136 | 108 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 𝑚 ⊆ 𝑑) |
137 | 134, 135,
136, 113 | syl12anc 836 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑤 ∈ 𝐵 (𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑)) |
138 | 132, 133,
137, 128 | syl3anbrc 1343 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → 〈𝑛, 𝑑〉 ∈ 𝑆) |
139 | | fveq2 6920 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 〈𝑛, 𝑑〉 → (1st ‘𝑥) = (1st
‘〈𝑛, 𝑑〉)) |
140 | | fveq2 6920 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 〈𝑛, 𝑑〉 → (𝑓‘𝑥) = (𝑓‘〈𝑛, 𝑑〉)) |
141 | 139, 140 | sseq12d 4042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 〈𝑛, 𝑑〉 → ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ↔ (1st ‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉))) |
142 | | fveq2 6920 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 = 〈𝑛, 𝑑〉 → (2nd ‘𝑥) = (2nd
‘〈𝑛, 𝑑〉)) |
143 | 140, 142 | sseq12d 4042 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 = 〈𝑛, 𝑑〉 → ((𝑓‘𝑥) ⊆ (2nd ‘𝑥) ↔ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉))) |
144 | 141, 143 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 = 〈𝑛, 𝑑〉 → (((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) ↔ ((1st
‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉)))) |
145 | 144 | rspcv 3631 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(〈𝑛, 𝑑〉 ∈ 𝑆 → (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((1st
‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉)))) |
146 | 138, 145 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((1st
‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉)))) |
147 | 116, 117 | op1st 8038 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1st ‘〈𝑛, 𝑑〉) = 𝑛 |
148 | 147 | sseq1i 4037 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((1st ‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ↔ 𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉)) |
149 | 116, 117 | op2nd 8039 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(2nd ‘〈𝑛, 𝑑〉) = 𝑑 |
150 | 149 | sseq2i 4038 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉) ↔ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑) |
151 | 148, 150 | anbi12i 627 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1st ‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉)) ↔ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) |
152 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → 𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉)) |
153 | | simprl 770 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → 𝑡 ∈ 𝑛) |
154 | 153 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → 𝑡 ∈ 𝑛) |
155 | 152, 154 | sseldd 4009 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → 𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉)) |
156 | | simprr 772 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑) |
157 | | simplrr 777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → 𝑑 ⊆ 𝑜) |
158 | 157 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → 𝑑 ⊆ 𝑜) |
159 | 156, 158 | sstrd 4019 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜) |
160 | 155, 159 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) ∧ (𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑)) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜)) |
161 | 160 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ((𝑛 ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑑) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))) |
162 | 151, 161 | biimtrid 242 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (((1st
‘〈𝑛, 𝑑〉) ⊆ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ (2nd
‘〈𝑛, 𝑑〉)) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))) |
163 | 146, 162 | syldc 48 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑥 ∈
𝑆 ((1st
‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))) |
164 | 163 | exp4c 432 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝑆 ((1st
‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))))) |
165 | 164 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜)) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))))) |
166 | 165 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ((𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜)) → ((𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑)) → ((𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚)) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))))) |
167 | 166 | imp41 425 |
. . . . . . . . . . . . . . . 16
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜)) |
168 | | eleq2 2833 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑓‘〈𝑛, 𝑑〉) → (𝑡 ∈ 𝑏 ↔ 𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉))) |
169 | | sseq1 4034 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = (𝑓‘〈𝑛, 𝑑〉) → (𝑏 ⊆ 𝑜 ↔ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜)) |
170 | 168, 169 | anbi12d 631 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑓‘〈𝑛, 𝑑〉) → ((𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜) ↔ (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜))) |
171 | 170 | rspcev 3635 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑓‘〈𝑛, 𝑑〉) ∈ ran 𝑓 ∧ (𝑡 ∈ (𝑓‘〈𝑛, 𝑑〉) ∧ (𝑓‘〈𝑛, 𝑑〉) ⊆ 𝑜)) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) |
172 | 131, 167,
171 | syl2anc 583 |
. . . . . . . . . . . . . . 15
⊢
(((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) ∧ (𝑛 ∈ 𝑐 ∧ (𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) |
173 | 99, 172 | rexlimddv 3167 |
. . . . . . . . . . . . . 14
⊢
((((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) ∧ (𝑚 ∈ 𝐵 ∧ (𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) |
174 | 89, 173 | rexlimddv 3167 |
. . . . . . . . . . . . 13
⊢
(((((𝐵 ∈
TopBases ∧ 𝐽 ∈
2ndω) ∧ (𝑐 ∈ TopBases ∧ (𝑐 ≼ ω ∧ (topGen‘𝑐) = 𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) ∧ (𝑑 ∈ 𝑐 ∧ (𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) |
175 | 75, 174 | rexlimddv 3167 |
. . . . . . . . . . . 12
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) ∧ (𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜))) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) |
176 | 175 | expr 456 |
. . . . . . . . . . 11
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ((𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜) → ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜))) |
177 | 176 | ralrimivv 3206 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ∀𝑜 ∈ 𝐽 ∀𝑡 ∈ 𝑜 ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) |
178 | | basgen2 23017 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ∀𝑜 ∈ 𝐽 ∀𝑡 ∈ 𝑜 ∃𝑏 ∈ ran 𝑓(𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜)) → (topGen‘ran 𝑓) = 𝐽) |
179 | 61, 68, 177, 178 | syl3anc 1371 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → (topGen‘ran
𝑓) = 𝐽) |
180 | 179, 61 | eqeltrd 2844 |
. . . . . . . 8
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → (topGen‘ran
𝑓) ∈
Top) |
181 | | tgclb 22998 |
. . . . . . . 8
⊢ (ran
𝑓 ∈ TopBases ↔
(topGen‘ran 𝑓) ∈
Top) |
182 | 180, 181 | sylibr 234 |
. . . . . . 7
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ∈
TopBases) |
183 | | omelon 9715 |
. . . . . . . . . 10
⊢ ω
∈ On |
184 | 24 | adantr 480 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑆 ≼ ω) |
185 | | ondomen 10106 |
. . . . . . . . . 10
⊢ ((ω
∈ On ∧ 𝑆 ≼
ω) → 𝑆 ∈
dom card) |
186 | 183, 184,
185 | sylancr 586 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑆 ∈ dom card) |
187 | 100 | ad2antrl 727 |
. . . . . . . . . 10
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑓 Fn 𝑆) |
188 | | dffn4 6840 |
. . . . . . . . . 10
⊢ (𝑓 Fn 𝑆 ↔ 𝑓:𝑆–onto→ran 𝑓) |
189 | 187, 188 | sylib 218 |
. . . . . . . . 9
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝑓:𝑆–onto→ran 𝑓) |
190 | | fodomnum 10126 |
. . . . . . . . 9
⊢ (𝑆 ∈ dom card → (𝑓:𝑆–onto→ran 𝑓 → ran 𝑓 ≼ 𝑆)) |
191 | 186, 189,
190 | sylc 65 |
. . . . . . . 8
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ≼ 𝑆) |
192 | | domtr 9067 |
. . . . . . . 8
⊢ ((ran
𝑓 ≼ 𝑆 ∧ 𝑆 ≼ ω) → ran 𝑓 ≼
ω) |
193 | 191, 184,
192 | syl2anc 583 |
. . . . . . 7
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ran 𝑓 ≼
ω) |
194 | 179 | eqcomd 2746 |
. . . . . . 7
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → 𝐽 = (topGen‘ran 𝑓)) |
195 | | breq1 5169 |
. . . . . . . . 9
⊢ (𝑏 = ran 𝑓 → (𝑏 ≼ ω ↔ ran 𝑓 ≼
ω)) |
196 | | sseq1 4034 |
. . . . . . . . 9
⊢ (𝑏 = ran 𝑓 → (𝑏 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵)) |
197 | | fveq2 6920 |
. . . . . . . . . 10
⊢ (𝑏 = ran 𝑓 → (topGen‘𝑏) = (topGen‘ran 𝑓)) |
198 | 197 | eqeq2d 2751 |
. . . . . . . . 9
⊢ (𝑏 = ran 𝑓 → (𝐽 = (topGen‘𝑏) ↔ 𝐽 = (topGen‘ran 𝑓))) |
199 | 195, 196,
198 | 3anbi123d 1436 |
. . . . . . . 8
⊢ (𝑏 = ran 𝑓 → ((𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)) ↔ (ran 𝑓 ≼ ω ∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = (topGen‘ran 𝑓)))) |
200 | 199 | rspcev 3635 |
. . . . . . 7
⊢ ((ran
𝑓 ∈ TopBases ∧
(ran 𝑓 ≼ ω
∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = (topGen‘ran 𝑓))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))) |
201 | 182, 193,
63, 194, 200 | syl13anc 1372 |
. . . . . 6
⊢ ((((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) ∧ (𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥)))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))) |
202 | 201 | ex 412 |
. . . . 5
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ((𝑓:𝑆⟶𝐵 ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))) |
203 | 58, 202 | sylbid 240 |
. . . 4
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ((𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))) |
204 | 203 | exlimdv 1932 |
. . 3
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → (∃𝑓(𝑓:𝑆⟶( I ‘𝐵) ∧ ∀𝑥 ∈ 𝑆 ((1st ‘𝑥) ⊆ (𝑓‘𝑥) ∧ (𝑓‘𝑥) ⊆ (2nd ‘𝑥))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏)))) |
205 | 55, 204 | mpd 15 |
. 2
⊢ (((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
∧ (𝑐 ∈ TopBases
∧ (𝑐 ≼ ω
∧ (topGen‘𝑐) =
𝐽))) → ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))) |
206 | 3, 205 | rexlimddv 3167 |
1
⊢ ((𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω)
→ ∃𝑏 ∈
TopBases (𝑏 ≼ ω
∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = (topGen‘𝑏))) |