Step | Hyp | Ref
| Expression |
1 | | is2ndc 21059 |
. 2
⊢ (𝐽 ∈ 2nd𝜔
↔ ∃𝑏 ∈
TopBases (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝐽)) |
2 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
3 | | difss 3699 |
. . . . . . . . 9
⊢ (𝑏 ∖ {∅}) ⊆
𝑏 |
4 | | ssdomg 7887 |
. . . . . . . . 9
⊢ (𝑏 ∈ V → ((𝑏 ∖ {∅}) ⊆
𝑏 → (𝑏 ∖ {∅}) ≼
𝑏)) |
5 | 2, 3, 4 | mp2 9 |
. . . . . . . 8
⊢ (𝑏 ∖ {∅}) ≼
𝑏 |
6 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) → 𝑏 ≼
ω) |
7 | | domtr 7895 |
. . . . . . . 8
⊢ (((𝑏 ∖ {∅}) ≼
𝑏 ∧ 𝑏 ≼ ω) → (𝑏 ∖ {∅}) ≼
ω) |
8 | 5, 6, 7 | sylancr 694 |
. . . . . . 7
⊢ ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) → (𝑏 ∖ {∅}) ≼
ω) |
9 | | eldifsn 4260 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝑏 ∖ {∅}) ↔ (𝑦 ∈ 𝑏 ∧ 𝑦 ≠ ∅)) |
10 | | n0 3890 |
. . . . . . . . . 10
⊢ (𝑦 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝑦) |
11 | | elunii 4377 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑏) → 𝑧 ∈ ∪ 𝑏) |
12 | | simpl 472 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑏) → 𝑧 ∈ 𝑦) |
13 | 11, 12 | jca 553 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝑏) → (𝑧 ∈ ∪ 𝑏 ∧ 𝑧 ∈ 𝑦)) |
14 | 13 | expcom 450 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑏 → (𝑧 ∈ 𝑦 → (𝑧 ∈ ∪ 𝑏 ∧ 𝑧 ∈ 𝑦))) |
15 | 14 | eximdv 1833 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ 𝑏 → (∃𝑧 𝑧 ∈ 𝑦 → ∃𝑧(𝑧 ∈ ∪ 𝑏 ∧ 𝑧 ∈ 𝑦))) |
16 | 15 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ 𝑏 ∧ ∃𝑧 𝑧 ∈ 𝑦) → ∃𝑧(𝑧 ∈ ∪ 𝑏 ∧ 𝑧 ∈ 𝑦)) |
17 | | df-rex 2902 |
. . . . . . . . . . 11
⊢
(∃𝑧 ∈
∪ 𝑏𝑧 ∈ 𝑦 ↔ ∃𝑧(𝑧 ∈ ∪ 𝑏 ∧ 𝑧 ∈ 𝑦)) |
18 | 16, 17 | sylibr 223 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝑏 ∧ ∃𝑧 𝑧 ∈ 𝑦) → ∃𝑧 ∈ ∪ 𝑏𝑧 ∈ 𝑦) |
19 | 10, 18 | sylan2b 491 |
. . . . . . . . 9
⊢ ((𝑦 ∈ 𝑏 ∧ 𝑦 ≠ ∅) → ∃𝑧 ∈ ∪ 𝑏𝑧 ∈ 𝑦) |
20 | 9, 19 | sylbi 206 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝑏 ∖ {∅}) → ∃𝑧 ∈ ∪ 𝑏𝑧 ∈ 𝑦) |
21 | 20 | rgen 2906 |
. . . . . . 7
⊢
∀𝑦 ∈
(𝑏 ∖
{∅})∃𝑧 ∈
∪ 𝑏𝑧 ∈ 𝑦 |
22 | | vuniex 6852 |
. . . . . . . 8
⊢ ∪ 𝑏
∈ V |
23 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑧 = (𝑓‘𝑦) → (𝑧 ∈ 𝑦 ↔ (𝑓‘𝑦) ∈ 𝑦)) |
24 | 22, 23 | axcc4dom 9146 |
. . . . . . 7
⊢ (((𝑏 ∖ {∅}) ≼
ω ∧ ∀𝑦
∈ (𝑏 ∖
{∅})∃𝑧 ∈
∪ 𝑏𝑧 ∈ 𝑦) → ∃𝑓(𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) |
25 | 8, 21, 24 | sylancl 693 |
. . . . . 6
⊢ ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) →
∃𝑓(𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) |
26 | | frn 5966 |
. . . . . . . . 9
⊢ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
→ ran 𝑓 ⊆ ∪ 𝑏) |
27 | 26 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → ran 𝑓 ⊆ ∪ 𝑏) |
28 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
29 | 28 | rnex 6992 |
. . . . . . . . 9
⊢ ran 𝑓 ∈ V |
30 | 29 | elpw 4114 |
. . . . . . . 8
⊢ (ran
𝑓 ∈ 𝒫 ∪ 𝑏
↔ ran 𝑓 ⊆ ∪ 𝑏) |
31 | 27, 30 | sylibr 223 |
. . . . . . 7
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → ran 𝑓 ∈ 𝒫 ∪ 𝑏) |
32 | | omelon 8426 |
. . . . . . . . . . 11
⊢ ω
∈ On |
33 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → 𝑏 ≼ ω) |
34 | | ondomen 8743 |
. . . . . . . . . . 11
⊢ ((ω
∈ On ∧ 𝑏 ≼
ω) → 𝑏 ∈
dom card) |
35 | 32, 33, 34 | sylancr 694 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → 𝑏 ∈ dom card) |
36 | | ssnum 8745 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ dom card ∧ (𝑏 ∖ {∅}) ⊆
𝑏) → (𝑏 ∖ {∅}) ∈ dom
card) |
37 | 35, 3, 36 | sylancl 693 |
. . . . . . . . 9
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → (𝑏 ∖ {∅}) ∈ dom
card) |
38 | | ffn 5958 |
. . . . . . . . . . 11
⊢ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
→ 𝑓 Fn (𝑏 ∖
{∅})) |
39 | 38 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → 𝑓 Fn (𝑏 ∖ {∅})) |
40 | | dffn4 6034 |
. . . . . . . . . 10
⊢ (𝑓 Fn (𝑏 ∖ {∅}) ↔ 𝑓:(𝑏 ∖ {∅})–onto→ran 𝑓) |
41 | 39, 40 | sylib 207 |
. . . . . . . . 9
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → 𝑓:(𝑏 ∖ {∅})–onto→ran 𝑓) |
42 | | fodomnum 8763 |
. . . . . . . . 9
⊢ ((𝑏 ∖ {∅}) ∈ dom
card → (𝑓:(𝑏 ∖ {∅})–onto→ran 𝑓 → ran 𝑓 ≼ (𝑏 ∖ {∅}))) |
43 | 37, 41, 42 | sylc 63 |
. . . . . . . 8
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → ran 𝑓 ≼ (𝑏 ∖ {∅})) |
44 | 8 | adantr 480 |
. . . . . . . 8
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → (𝑏 ∖ {∅}) ≼
ω) |
45 | | domtr 7895 |
. . . . . . . 8
⊢ ((ran
𝑓 ≼ (𝑏 ∖ {∅}) ∧ (𝑏 ∖ {∅}) ≼
ω) → ran 𝑓
≼ ω) |
46 | 43, 44, 45 | syl2anc 691 |
. . . . . . 7
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → ran 𝑓 ≼ ω) |
47 | | tgcl 20584 |
. . . . . . . . . 10
⊢ (𝑏 ∈ TopBases →
(topGen‘𝑏) ∈
Top) |
48 | 47 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → (topGen‘𝑏) ∈ Top) |
49 | | unitg 20582 |
. . . . . . . . . . . 12
⊢ (𝑏 ∈ V → ∪ (topGen‘𝑏) = ∪ 𝑏) |
50 | 2, 49 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ∪ (topGen‘𝑏) = ∪ 𝑏 |
51 | 50 | eqcomi 2619 |
. . . . . . . . . 10
⊢ ∪ 𝑏 =
∪ (topGen‘𝑏) |
52 | 51 | clsss3 20673 |
. . . . . . . . 9
⊢
(((topGen‘𝑏)
∈ Top ∧ ran 𝑓
⊆ ∪ 𝑏) → ((cls‘(topGen‘𝑏))‘ran 𝑓) ⊆ ∪ 𝑏) |
53 | 48, 27, 52 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → ((cls‘(topGen‘𝑏))‘ran 𝑓) ⊆ ∪ 𝑏) |
54 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑦 → 𝑦 ≠ ∅) |
55 | 54 | anim2i 591 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ 𝑏 ∧ 𝑥 ∈ 𝑦) → (𝑦 ∈ 𝑏 ∧ 𝑦 ≠ ∅)) |
56 | 55, 9 | sylibr 223 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ 𝑏 ∧ 𝑥 ∈ 𝑦) → 𝑦 ∈ (𝑏 ∖ {∅})) |
57 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑓 Fn (𝑏 ∖ {∅}) ∧ 𝑦 ∈ (𝑏 ∖ {∅})) → (𝑓‘𝑦) ∈ ran 𝑓) |
58 | 38, 57 | sylan 487 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ 𝑦 ∈ (𝑏 ∖ {∅})) →
(𝑓‘𝑦) ∈ ran 𝑓) |
59 | | inelcm 3984 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑓‘𝑦) ∈ 𝑦 ∧ (𝑓‘𝑦) ∈ ran 𝑓) → (𝑦 ∩ ran 𝑓) ≠ ∅) |
60 | 59 | expcom 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑓‘𝑦) ∈ ran 𝑓 → ((𝑓‘𝑦) ∈ 𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅)) |
61 | 58, 60 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ 𝑦 ∈ (𝑏 ∖ {∅})) →
((𝑓‘𝑦) ∈ 𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅)) |
62 | 61 | ex 449 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
→ (𝑦 ∈ (𝑏 ∖ {∅}) →
((𝑓‘𝑦) ∈ 𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅))) |
63 | 62 | a2d 29 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
→ ((𝑦 ∈ (𝑏 ∖ {∅}) →
(𝑓‘𝑦) ∈ 𝑦) → (𝑦 ∈ (𝑏 ∖ {∅}) → (𝑦 ∩ ran 𝑓) ≠ ∅))) |
64 | 56, 63 | syl7 72 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
→ ((𝑦 ∈ (𝑏 ∖ {∅}) →
(𝑓‘𝑦) ∈ 𝑦) → ((𝑦 ∈ 𝑏 ∧ 𝑥 ∈ 𝑦) → (𝑦 ∩ ran 𝑓) ≠ ∅))) |
65 | 64 | exp4a 631 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
→ ((𝑦 ∈ (𝑏 ∖ {∅}) →
(𝑓‘𝑦) ∈ 𝑦) → (𝑦 ∈ 𝑏 → (𝑥 ∈ 𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅)))) |
66 | 65 | ralimdv2 2944 |
. . . . . . . . . . . . 13
⊢ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
→ (∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦 → ∀𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅))) |
67 | 66 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦) → ∀𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅)) |
68 | 67 | ad2antlr 759 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) ∧ 𝑥 ∈ ∪ 𝑏) → ∀𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅)) |
69 | | eqidd 2611 |
. . . . . . . . . . . 12
⊢ ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) ∧ 𝑥 ∈ ∪ 𝑏) → (topGen‘𝑏) = (topGen‘𝑏)) |
70 | 51 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) ∧ 𝑥 ∈ ∪ 𝑏) → ∪ 𝑏 =
∪ (topGen‘𝑏)) |
71 | | simplll 794 |
. . . . . . . . . . . 12
⊢ ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) ∧ 𝑥 ∈ ∪ 𝑏) → 𝑏 ∈ TopBases) |
72 | 27 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) ∧ 𝑥 ∈ ∪ 𝑏) → ran 𝑓 ⊆ ∪ 𝑏) |
73 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) ∧ 𝑥 ∈ ∪ 𝑏) → 𝑥 ∈ ∪ 𝑏) |
74 | 69, 70, 71, 72, 73 | elcls3 20697 |
. . . . . . . . . . 11
⊢ ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) ∧ 𝑥 ∈ ∪ 𝑏) → (𝑥 ∈ ((cls‘(topGen‘𝑏))‘ran 𝑓) ↔ ∀𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 → (𝑦 ∩ ran 𝑓) ≠ ∅))) |
75 | 68, 74 | mpbird 246 |
. . . . . . . . . 10
⊢ ((((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) ∧ 𝑥 ∈ ∪ 𝑏) → 𝑥 ∈ ((cls‘(topGen‘𝑏))‘ran 𝑓)) |
76 | 75 | ex 449 |
. . . . . . . . 9
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → (𝑥 ∈ ∪ 𝑏 → 𝑥 ∈ ((cls‘(topGen‘𝑏))‘ran 𝑓))) |
77 | 76 | ssrdv 3574 |
. . . . . . . 8
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → ∪ 𝑏 ⊆
((cls‘(topGen‘𝑏))‘ran 𝑓)) |
78 | 53, 77 | eqssd 3585 |
. . . . . . 7
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → ((cls‘(topGen‘𝑏))‘ran 𝑓) = ∪ 𝑏) |
79 | | breq1 4586 |
. . . . . . . . 9
⊢ (𝑥 = ran 𝑓 → (𝑥 ≼ ω ↔ ran 𝑓 ≼
ω)) |
80 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = ran 𝑓 → ((cls‘(topGen‘𝑏))‘𝑥) = ((cls‘(topGen‘𝑏))‘ran 𝑓)) |
81 | 80 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑥 = ran 𝑓 → (((cls‘(topGen‘𝑏))‘𝑥) = ∪ 𝑏 ↔
((cls‘(topGen‘𝑏))‘ran 𝑓) = ∪ 𝑏)) |
82 | 79, 81 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑥 = ran 𝑓 → ((𝑥 ≼ ω ∧
((cls‘(topGen‘𝑏))‘𝑥) = ∪ 𝑏) ↔ (ran 𝑓 ≼ ω ∧
((cls‘(topGen‘𝑏))‘ran 𝑓) = ∪ 𝑏))) |
83 | 82 | rspcev 3282 |
. . . . . . 7
⊢ ((ran
𝑓 ∈ 𝒫 ∪ 𝑏
∧ (ran 𝑓 ≼
ω ∧ ((cls‘(topGen‘𝑏))‘ran 𝑓) = ∪ 𝑏)) → ∃𝑥 ∈ 𝒫 ∪ 𝑏(𝑥 ≼ ω ∧
((cls‘(topGen‘𝑏))‘𝑥) = ∪ 𝑏)) |
84 | 31, 46, 78, 83 | syl12anc 1316 |
. . . . . 6
⊢ (((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) ∧ (𝑓:(𝑏 ∖ {∅})⟶∪ 𝑏
∧ ∀𝑦 ∈
(𝑏 ∖ {∅})(𝑓‘𝑦) ∈ 𝑦)) → ∃𝑥 ∈ 𝒫 ∪ 𝑏(𝑥 ≼ ω ∧
((cls‘(topGen‘𝑏))‘𝑥) = ∪ 𝑏)) |
85 | 25, 84 | exlimddv 1850 |
. . . . 5
⊢ ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) →
∃𝑥 ∈ 𝒫
∪ 𝑏(𝑥 ≼ ω ∧
((cls‘(topGen‘𝑏))‘𝑥) = ∪ 𝑏)) |
86 | | unieq 4380 |
. . . . . . . 8
⊢
((topGen‘𝑏) =
𝐽 → ∪ (topGen‘𝑏) = ∪ 𝐽) |
87 | | 2ndcsep.1 |
. . . . . . . 8
⊢ 𝑋 = ∪
𝐽 |
88 | 86, 51, 87 | 3eqtr4g 2669 |
. . . . . . 7
⊢
((topGen‘𝑏) =
𝐽 → ∪ 𝑏 =
𝑋) |
89 | 88 | pweqd 4113 |
. . . . . 6
⊢
((topGen‘𝑏) =
𝐽 → 𝒫 ∪ 𝑏 =
𝒫 𝑋) |
90 | | fveq2 6103 |
. . . . . . . . 9
⊢
((topGen‘𝑏) =
𝐽 →
(cls‘(topGen‘𝑏)) = (cls‘𝐽)) |
91 | 90 | fveq1d 6105 |
. . . . . . . 8
⊢
((topGen‘𝑏) =
𝐽 →
((cls‘(topGen‘𝑏))‘𝑥) = ((cls‘𝐽)‘𝑥)) |
92 | 91, 88 | eqeq12d 2625 |
. . . . . . 7
⊢
((topGen‘𝑏) =
𝐽 →
(((cls‘(topGen‘𝑏))‘𝑥) = ∪ 𝑏 ↔ ((cls‘𝐽)‘𝑥) = 𝑋)) |
93 | 92 | anbi2d 736 |
. . . . . 6
⊢
((topGen‘𝑏) =
𝐽 → ((𝑥 ≼ ω ∧
((cls‘(topGen‘𝑏))‘𝑥) = ∪ 𝑏) ↔ (𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋))) |
94 | 89, 93 | rexeqbidv 3130 |
. . . . 5
⊢
((topGen‘𝑏) =
𝐽 → (∃𝑥 ∈ 𝒫 ∪ 𝑏(𝑥 ≼ ω ∧
((cls‘(topGen‘𝑏))‘𝑥) = ∪ 𝑏) ↔ ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋))) |
95 | 85, 94 | syl5ibcom 234 |
. . . 4
⊢ ((𝑏 ∈ TopBases ∧ 𝑏 ≼ ω) →
((topGen‘𝑏) = 𝐽 → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋))) |
96 | 95 | impr 647 |
. . 3
⊢ ((𝑏 ∈ TopBases ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽)) → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋)) |
97 | 96 | rexlimiva 3010 |
. 2
⊢
(∃𝑏 ∈
TopBases (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝐽) → ∃𝑥 ∈ 𝒫 𝑋(𝑥 ≼ ω ∧ ((cls‘𝐽)‘𝑥) = 𝑋)) |
98 | 1, 97 | sylbi 206 |
1
⊢ (𝐽 ∈ 2nd𝜔
→ ∃𝑥 ∈
𝒫 𝑋(𝑥 ≼ ω ∧
((cls‘𝐽)‘𝑥) = 𝑋)) |