Step | Hyp | Ref
| Expression |
1 | | isbasis2g 12802 |
. . . . 5
⊢ (𝐵 ∈ TopBases → (𝐵 ∈ TopBases ↔
∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ (𝑦 ∩ 𝑧)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑦 ∩ 𝑧)))) |
2 | 1 | ibi 175 |
. . . 4
⊢ (𝐵 ∈ TopBases →
∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ (𝑦 ∩ 𝑧)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑦 ∩ 𝑧))) |
3 | | ineq1 3321 |
. . . . . . 7
⊢ (𝑦 = 𝐶 → (𝑦 ∩ 𝑧) = (𝐶 ∩ 𝑧)) |
4 | | sseq2 3171 |
. . . . . . . . . 10
⊢ ((𝑦 ∩ 𝑧) = (𝐶 ∩ 𝑧) → (𝑥 ⊆ (𝑦 ∩ 𝑧) ↔ 𝑥 ⊆ (𝐶 ∩ 𝑧))) |
5 | 4 | anbi2d 461 |
. . . . . . . . 9
⊢ ((𝑦 ∩ 𝑧) = (𝐶 ∩ 𝑧) → ((𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑦 ∩ 𝑧)) ↔ (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝑧)))) |
6 | 5 | rexbidv 2471 |
. . . . . . . 8
⊢ ((𝑦 ∩ 𝑧) = (𝐶 ∩ 𝑧) → (∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑦 ∩ 𝑧)) ↔ ∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝑧)))) |
7 | 6 | raleqbi1dv 2673 |
. . . . . . 7
⊢ ((𝑦 ∩ 𝑧) = (𝐶 ∩ 𝑧) → (∀𝑤 ∈ (𝑦 ∩ 𝑧)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑦 ∩ 𝑧)) ↔ ∀𝑤 ∈ (𝐶 ∩ 𝑧)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝑧)))) |
8 | 3, 7 | syl 14 |
. . . . . 6
⊢ (𝑦 = 𝐶 → (∀𝑤 ∈ (𝑦 ∩ 𝑧)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑦 ∩ 𝑧)) ↔ ∀𝑤 ∈ (𝐶 ∩ 𝑧)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝑧)))) |
9 | | ineq2 3322 |
. . . . . . 7
⊢ (𝑧 = 𝐷 → (𝐶 ∩ 𝑧) = (𝐶 ∩ 𝐷)) |
10 | | sseq2 3171 |
. . . . . . . . . 10
⊢ ((𝐶 ∩ 𝑧) = (𝐶 ∩ 𝐷) → (𝑥 ⊆ (𝐶 ∩ 𝑧) ↔ 𝑥 ⊆ (𝐶 ∩ 𝐷))) |
11 | 10 | anbi2d 461 |
. . . . . . . . 9
⊢ ((𝐶 ∩ 𝑧) = (𝐶 ∩ 𝐷) → ((𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝑧)) ↔ (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))) |
12 | 11 | rexbidv 2471 |
. . . . . . . 8
⊢ ((𝐶 ∩ 𝑧) = (𝐶 ∩ 𝐷) → (∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝑧)) ↔ ∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))) |
13 | 12 | raleqbi1dv 2673 |
. . . . . . 7
⊢ ((𝐶 ∩ 𝑧) = (𝐶 ∩ 𝐷) → (∀𝑤 ∈ (𝐶 ∩ 𝑧)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝑧)) ↔ ∀𝑤 ∈ (𝐶 ∩ 𝐷)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))) |
14 | 9, 13 | syl 14 |
. . . . . 6
⊢ (𝑧 = 𝐷 → (∀𝑤 ∈ (𝐶 ∩ 𝑧)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝑧)) ↔ ∀𝑤 ∈ (𝐶 ∩ 𝐷)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))) |
15 | 8, 14 | rspc2v 2847 |
. . . . 5
⊢ ((𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ (𝑦 ∩ 𝑧)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑦 ∩ 𝑧)) → ∀𝑤 ∈ (𝐶 ∩ 𝐷)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))) |
16 | | eleq1 2233 |
. . . . . . . 8
⊢ (𝑤 = 𝐴 → (𝑤 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥)) |
17 | 16 | anbi1d 462 |
. . . . . . 7
⊢ (𝑤 = 𝐴 → ((𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)) ↔ (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))) |
18 | 17 | rexbidv 2471 |
. . . . . 6
⊢ (𝑤 = 𝐴 → (∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)) ↔ ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))) |
19 | 18 | rspccv 2831 |
. . . . 5
⊢
(∀𝑤 ∈
(𝐶 ∩ 𝐷)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)) → (𝐴 ∈ (𝐶 ∩ 𝐷) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))) |
20 | 15, 19 | syl6com 35 |
. . . 4
⊢
(∀𝑦 ∈
𝐵 ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ (𝑦 ∩ 𝑧)∃𝑥 ∈ 𝐵 (𝑤 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑦 ∩ 𝑧)) → ((𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐴 ∈ (𝐶 ∩ 𝐷) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷))))) |
21 | 2, 20 | syl 14 |
. . 3
⊢ (𝐵 ∈ TopBases → ((𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐴 ∈ (𝐶 ∩ 𝐷) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷))))) |
22 | 21 | expd 256 |
. 2
⊢ (𝐵 ∈ TopBases → (𝐶 ∈ 𝐵 → (𝐷 ∈ 𝐵 → (𝐴 ∈ (𝐶 ∩ 𝐷) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷)))))) |
23 | 22 | imp43 353 |
1
⊢ (((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵) ∧ (𝐷 ∈ 𝐵 ∧ 𝐴 ∈ (𝐶 ∩ 𝐷))) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷))) |