Step | Hyp | Ref
| Expression |
1 | | is2ndc 21059 |
. . 3
⊢ (𝐽 ∈ 2nd𝜔
↔ ∃𝑏 ∈
TopBases (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝐽)) |
2 | | omex 8423 |
. . . . . . 7
⊢ ω
∈ V |
3 | 2 | brdom 7853 |
. . . . . 6
⊢ (𝑏 ≼ ω ↔
∃𝑓 𝑓:𝑏–1-1→ω) |
4 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ ran 𝑓 |
5 | | f1f 6014 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:𝑏–1-1→ω → 𝑓:𝑏⟶ω) |
6 | | frn 5966 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓:𝑏⟶ω → ran 𝑓 ⊆ ω) |
7 | 5, 6 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓:𝑏–1-1→ω → ran 𝑓 ⊆ ω) |
8 | 7 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ran 𝑓 ⊆ ω) |
9 | 4, 8 | syl5ss 3579 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆
ω) |
10 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆
ω) |
11 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔
(𝐵 ∈
(topGen‘𝑏) ∧
𝐵 ≠
∅)) |
12 | | n0 3890 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐵 ≠ ∅ ↔
∃𝑦 𝑦 ∈ 𝐵) |
13 | | tg2 20580 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵)) |
14 | | omsson 6961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ω
⊆ On |
15 | 9, 14 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆
On) |
16 | 15 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆
On) |
17 | | f1fn 6015 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑓:𝑏–1-1→ω → 𝑓 Fn 𝑏) |
18 | 17 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓 Fn 𝑏) |
19 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝑏) |
20 | | fnfvelrn 6264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑓 Fn 𝑏 ∧ 𝑧 ∈ 𝑏) → (𝑓‘𝑧) ∈ ran 𝑓) |
21 | 18, 19, 20 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (𝑓‘𝑧) ∈ ran 𝑓) |
22 | | f1f1orn 6061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑓:𝑏–1-1→ω → 𝑓:𝑏–1-1-onto→ran
𝑓) |
23 | 22 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑓:𝑏–1-1-onto→ran
𝑓) |
24 | | f1ocnvfv1 6432 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑓:𝑏–1-1-onto→ran
𝑓 ∧ 𝑧 ∈ 𝑏) → (◡𝑓‘(𝑓‘𝑧)) = 𝑧) |
25 | 23, 19, 24 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (◡𝑓‘(𝑓‘𝑧)) = 𝑧) |
26 | | simprrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ⊆ 𝐵) |
27 | | selpw 4115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵) |
28 | 26, 27 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ 𝒫 𝐵) |
29 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑦 ∈ 𝑧) |
30 | | ne0i 3880 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 ∈ 𝑧 → 𝑧 ≠ ∅) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ≠ ∅) |
32 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 ∈ (𝒫 𝐵 ∖ {∅}) ↔
(𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ≠ ∅)) |
33 | 28, 31, 32 | sylanbrc 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → 𝑧 ∈ (𝒫 𝐵 ∖ {∅})) |
34 | 25, 33 | eqeltrd 2688 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → (◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})) |
35 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑛 = (𝑓‘𝑧) → (◡𝑓‘𝑛) = (◡𝑓‘(𝑓‘𝑧))) |
36 | 35 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑛 = (𝑓‘𝑧) → ((◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅}))) |
37 | 36 | rspcev 3282 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑓‘𝑧) ∈ ran 𝑓 ∧ (◡𝑓‘(𝑓‘𝑧)) ∈ (𝒫 𝐵 ∖ {∅})) → ∃𝑛 ∈ ran 𝑓(◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})) |
38 | 21, 34, 37 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∃𝑛 ∈ ran 𝑓(◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})) |
39 | | rabn0 3912 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ({𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅ ↔
∃𝑛 ∈ ran 𝑓(◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})) |
40 | 38, 39 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠
∅) |
41 | | onint 6887 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (({𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ⊆ On ∧ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ≠ ∅) →
∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) |
42 | 16, 40, 41 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ (𝑧 ∈ 𝑏 ∧ (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵))) → ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) |
43 | 42 | rexlimdvaa 3014 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (∃𝑧 ∈ 𝑏 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
44 | 13, 43 | syl5 33 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝑦 ∈ 𝐵) → ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
45 | 44 | expdimp 452 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
46 | 45 | exlimdv 1848 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (∃𝑦 𝑦 ∈ 𝐵 → ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
47 | 12, 46 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) ∧ 𝐵 ∈ (topGen‘𝑏)) → (𝐵 ≠ ∅ → ∩ {𝑛
∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
48 | 47 | expimpd 627 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → ((𝐵 ∈ (topGen‘𝑏) ∧ 𝐵 ≠ ∅) → ∩ {𝑛
∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
49 | 11, 48 | syl5bi 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛
∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
50 | 49 | impr 647 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛
∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) |
51 | 10, 50 | sseldd 3569 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → ∩ {𝑛
∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈
ω) |
52 | 51 | expr 641 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∩ {𝑛
∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈
ω)) |
53 | 52 | ralimdva 2945 |
. . . . . . . . . . . . . . 15
⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈
ω)) |
54 | 53 | imp 444 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈
ω) |
55 | 54 | adantrr 749 |
. . . . . . . . . . . . 13
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑥 ∈ 𝐴 ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈
ω) |
56 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) |
57 | 56 | fmpt 6289 |
. . . . . . . . . . . . 13
⊢
(∀𝑥 ∈
𝐴 ∩ {𝑛
∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ ω ↔
(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω) |
58 | 55, 57 | sylib 207 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω) |
59 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((◡𝑓‘𝑧) = if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) → ((◡𝑓‘𝑧) ≠ ∅ ↔ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) ≠
∅)) |
60 | | neeq1 2844 |
. . . . . . . . . . . . . . . . . . 19
⊢
(1𝑜 = if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) →
(1𝑜 ≠ ∅ ↔ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) ≠
∅)) |
61 | | 1n0 7462 |
. . . . . . . . . . . . . . . . . . 19
⊢
1𝑜 ≠ ∅ |
62 | 59, 60, 61 | elimhyp 4096 |
. . . . . . . . . . . . . . . . . 18
⊢ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) ≠
∅ |
63 | | n0 3890 |
. . . . . . . . . . . . . . . . . 18
⊢
(if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) ≠ ∅ ↔
∃𝑦 𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜)) |
64 | 62, 63 | mpbi 219 |
. . . . . . . . . . . . . . . . 17
⊢
∃𝑦 𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) |
65 | | 19.29r 1790 |
. . . . . . . . . . . . . . . . 17
⊢
((∃𝑦 𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃𝑦(𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) ∧ ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
66 | 64, 65 | mpan 702 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃𝑦(𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) ∧ ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) |
67 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ ∩ {𝑛
∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
68 | 50, 67 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) → (𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
69 | 68 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → 𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) |
70 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑛 = 𝑧 → (◡𝑓‘𝑛) = (◡𝑓‘𝑧)) |
71 | 70 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑛 = 𝑧 → ((◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅}) ↔ (◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))) |
72 | 71 | elrab 3331 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ (𝑧 ∈ ran 𝑓 ∧ (◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}))) |
73 | 72 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})) |
74 | 69, 73 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅})) |
75 | | eldifsn 4260 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((◡𝑓‘𝑧) ∈ (𝒫 𝐵 ∖ {∅}) ↔ ((◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (◡𝑓‘𝑧) ≠ ∅)) |
76 | 74, 75 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → ((◡𝑓‘𝑧) ∈ 𝒫 𝐵 ∧ (◡𝑓‘𝑧) ≠ ∅)) |
77 | 76 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (◡𝑓‘𝑧) ≠ ∅) |
78 | 77 | iftrued 4044 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) = (◡𝑓‘𝑧)) |
79 | 76 | simpld 474 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (◡𝑓‘𝑧) ∈ 𝒫 𝐵) |
80 | 79 | elpwid 4118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (◡𝑓‘𝑧) ⊆ 𝐵) |
81 | 78, 80 | eqsstrd 3602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) ⊆ 𝐵) |
82 | 81 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}))) ∧ 𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) → (𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) → 𝑦 ∈ 𝐵)) |
83 | 82 | exp31 628 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) → 𝑦 ∈ 𝐵)))) |
84 | 83 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) → 𝑦 ∈ 𝐵)))) |
85 | 84 | exp4a 631 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → (𝑥 ∈ 𝐴 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) → 𝑦 ∈ 𝐵))))) |
86 | 85 | com25 97 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → (𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) → (𝑥 ∈ 𝐴 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))))) |
87 | 86 | imp31 447 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜)) ∧ 𝑥 ∈ 𝐴) → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → (𝑧 = ∩
{𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))) |
88 | 87 | ralimdva 2945 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜)) →
(∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵))) |
89 | 88 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ 𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜)) ∧
∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)) |
90 | 89 | an32s 842 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜)) →
∀𝑥 ∈ 𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵)) |
91 | | rmoim 3374 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝐴 (𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} → 𝑦 ∈ 𝐵) → (∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃*𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
92 | 90, 91 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) ∧ 𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜)) →
(∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃*𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
93 | 92 | expimpd 627 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → ((𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) ∧ ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃*𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
94 | 93 | exlimdv 1848 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∃𝑦(𝑦 ∈ if((◡𝑓‘𝑧) ≠ ∅, (◡𝑓‘𝑧), 1𝑜) ∧ ∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → ∃*𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
95 | 66, 94 | syl5 33 |
. . . . . . . . . . . . . . 15
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅})) → (∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → ∃*𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
96 | 95 | impr 647 |
. . . . . . . . . . . . . 14
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∃*𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) |
97 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝑤 |
98 | | nfmpt1 4675 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) |
99 | | nfcv 2751 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝑧 |
100 | 97, 98, 99 | nfbr 4629 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 |
101 | | nfv 1830 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑤(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) |
102 | | breq1 4586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑥 → (𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ 𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧)) |
103 | | df-br 4584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ 〈𝑥, 𝑧〉 ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
104 | | df-mpt 4645 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})} |
105 | 104 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑧〉 ∈ (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) ↔ 〈𝑥, 𝑧〉 ∈ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})}) |
106 | | opabid 4907 |
. . . . . . . . . . . . . . . . . 18
⊢
(〈𝑥, 𝑧〉 ∈ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})} ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
107 | 103, 105,
106 | 3bitri 285 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
108 | 102, 107 | syl6bb 275 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑥 → (𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ (𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}))) |
109 | 100, 101,
108 | cbvmo 2494 |
. . . . . . . . . . . . . . 15
⊢
(∃*𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
110 | | df-rmo 2904 |
. . . . . . . . . . . . . . 15
⊢
(∃*𝑥 ∈
𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})} ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})) |
111 | 109, 110 | bitr4i 266 |
. . . . . . . . . . . . . 14
⊢
(∃*𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧 ↔ ∃*𝑥 ∈ 𝐴 𝑧 = ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}) |
112 | 96, 111 | sylibr 223 |
. . . . . . . . . . . . 13
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∃*𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧) |
113 | 112 | alrimiv 1842 |
. . . . . . . . . . . 12
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → ∀𝑧∃*𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧) |
114 | | dff12 6013 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω ↔ ((𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴⟶ω ∧ ∀𝑧∃*𝑤 𝑤(𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})})𝑧)) |
115 | 58, 113, 114 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ∩ {𝑛 ∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω) |
116 | | f1domg 7861 |
. . . . . . . . . . 11
⊢ (ω
∈ V → ((𝑥 ∈
𝐴 ↦ ∩ {𝑛
∈ ran 𝑓 ∣ (◡𝑓‘𝑛) ∈ (𝒫 𝐵 ∖ {∅})}):𝐴–1-1→ω → 𝐴 ≼ ω)) |
117 | 2, 115, 116 | mpsyl 66 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) ∧ (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) → 𝐴 ≼ ω) |
118 | 117 | ex 449 |
. . . . . . . . 9
⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)) |
119 | | difeq1 3683 |
. . . . . . . . . . . . 13
⊢
((topGen‘𝑏) =
𝐽 →
((topGen‘𝑏) ∖
{∅}) = (𝐽 ∖
{∅})) |
120 | 119 | eleq2d 2673 |
. . . . . . . . . . . 12
⊢
((topGen‘𝑏) =
𝐽 → (𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ 𝐵 ∈ (𝐽 ∖ {∅}))) |
121 | 120 | ralbidv 2969 |
. . . . . . . . . . 11
⊢
((topGen‘𝑏) =
𝐽 → (∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}))) |
122 | 121 | anbi1d 737 |
. . . . . . . . . 10
⊢
((topGen‘𝑏) =
𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) ↔ (∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵))) |
123 | 122 | imbi1d 330 |
. . . . . . . . 9
⊢
((topGen‘𝑏) =
𝐽 → (((∀𝑥 ∈ 𝐴 𝐵 ∈ ((topGen‘𝑏) ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω) ↔ ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))) |
124 | 118, 123 | syl5ibcom 234 |
. . . . . . . 8
⊢ ((𝑏 ∈ TopBases ∧ 𝑓:𝑏–1-1→ω) → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))) |
125 | 124 | ex 449 |
. . . . . . 7
⊢ (𝑏 ∈ TopBases → (𝑓:𝑏–1-1→ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))) |
126 | 125 | exlimdv 1848 |
. . . . . 6
⊢ (𝑏 ∈ TopBases →
(∃𝑓 𝑓:𝑏–1-1→ω → ((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))) |
127 | 3, 126 | syl5bi 231 |
. . . . 5
⊢ (𝑏 ∈ TopBases → (𝑏 ≼ ω →
((topGen‘𝑏) = 𝐽 → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)))) |
128 | 127 | impd 446 |
. . . 4
⊢ (𝑏 ∈ TopBases → ((𝑏 ≼ ω ∧
(topGen‘𝑏) = 𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω))) |
129 | 128 | rexlimiv 3009 |
. . 3
⊢
(∃𝑏 ∈
TopBases (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝐽) → ((∀𝑥 ∈ 𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)) |
130 | 1, 129 | sylbi 206 |
. 2
⊢ (𝐽 ∈ 2nd𝜔
→ ((∀𝑥 ∈
𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω)) |
131 | 130 | 3impib 1254 |
1
⊢ ((𝐽 ∈ 2nd𝜔
∧ ∀𝑥 ∈
𝐴 𝐵 ∈ (𝐽 ∖ {∅}) ∧ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) → 𝐴 ≼ ω) |