Step | Hyp | Ref
| Expression |
1 | | txval.1 |
. . . . . . . 8
⊢ 𝐵 = ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) |
2 | | xpeq1 5602 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑎 → (𝑥 × 𝑦) = (𝑎 × 𝑦)) |
3 | | xpeq2 5609 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑏 → (𝑎 × 𝑦) = (𝑎 × 𝑏)) |
4 | 2, 3 | cbvmpov 7361 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) = (𝑎 ∈ 𝑅, 𝑏 ∈ 𝑆 ↦ (𝑎 × 𝑏)) |
5 | 4 | rnmpo 7398 |
. . . . . . . 8
⊢ ran
(𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) = {𝑢 ∣ ∃𝑎 ∈ 𝑅 ∃𝑏 ∈ 𝑆 𝑢 = (𝑎 × 𝑏)} |
6 | 1, 5 | eqtri 2767 |
. . . . . . 7
⊢ 𝐵 = {𝑢 ∣ ∃𝑎 ∈ 𝑅 ∃𝑏 ∈ 𝑆 𝑢 = (𝑎 × 𝑏)} |
7 | 6 | abeq2i 2876 |
. . . . . 6
⊢ (𝑢 ∈ 𝐵 ↔ ∃𝑎 ∈ 𝑅 ∃𝑏 ∈ 𝑆 𝑢 = (𝑎 × 𝑏)) |
8 | | xpeq1 5602 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑐 → (𝑥 × 𝑦) = (𝑐 × 𝑦)) |
9 | | xpeq2 5609 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑑 → (𝑐 × 𝑦) = (𝑐 × 𝑑)) |
10 | 8, 9 | cbvmpov 7361 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) = (𝑐 ∈ 𝑅, 𝑑 ∈ 𝑆 ↦ (𝑐 × 𝑑)) |
11 | 10 | rnmpo 7398 |
. . . . . . . 8
⊢ ran
(𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) = {𝑣 ∣ ∃𝑐 ∈ 𝑅 ∃𝑑 ∈ 𝑆 𝑣 = (𝑐 × 𝑑)} |
12 | 1, 11 | eqtri 2767 |
. . . . . . 7
⊢ 𝐵 = {𝑣 ∣ ∃𝑐 ∈ 𝑅 ∃𝑑 ∈ 𝑆 𝑣 = (𝑐 × 𝑑)} |
13 | 12 | abeq2i 2876 |
. . . . . 6
⊢ (𝑣 ∈ 𝐵 ↔ ∃𝑐 ∈ 𝑅 ∃𝑑 ∈ 𝑆 𝑣 = (𝑐 × 𝑑)) |
14 | 7, 13 | anbi12i 626 |
. . . . 5
⊢ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ↔ (∃𝑎 ∈ 𝑅 ∃𝑏 ∈ 𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐 ∈ 𝑅 ∃𝑑 ∈ 𝑆 𝑣 = (𝑐 × 𝑑))) |
15 | | reeanv 3294 |
. . . . 5
⊢
(∃𝑎 ∈
𝑅 ∃𝑐 ∈ 𝑅 (∃𝑏 ∈ 𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑 ∈ 𝑆 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑎 ∈ 𝑅 ∃𝑏 ∈ 𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑐 ∈ 𝑅 ∃𝑑 ∈ 𝑆 𝑣 = (𝑐 × 𝑑))) |
16 | 14, 15 | bitr4i 277 |
. . . 4
⊢ ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) ↔ ∃𝑎 ∈ 𝑅 ∃𝑐 ∈ 𝑅 (∃𝑏 ∈ 𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑 ∈ 𝑆 𝑣 = (𝑐 × 𝑑))) |
17 | | reeanv 3294 |
. . . . . 6
⊢
(∃𝑏 ∈
𝑆 ∃𝑑 ∈ 𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) ↔ (∃𝑏 ∈ 𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑 ∈ 𝑆 𝑣 = (𝑐 × 𝑑))) |
18 | | basis2 22082 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑅 ∈ TopBases ∧ 𝑎 ∈ 𝑅) ∧ (𝑐 ∈ 𝑅 ∧ 𝑢 ∈ (𝑎 ∩ 𝑐))) → ∃𝑥 ∈ 𝑅 (𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑎 ∩ 𝑐))) |
19 | 18 | exp43 436 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 ∈ TopBases → (𝑎 ∈ 𝑅 → (𝑐 ∈ 𝑅 → (𝑢 ∈ (𝑎 ∩ 𝑐) → ∃𝑥 ∈ 𝑅 (𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑎 ∩ 𝑐)))))) |
20 | 19 | imp42 426 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 ∈ TopBases ∧ (𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅)) ∧ 𝑢 ∈ (𝑎 ∩ 𝑐)) → ∃𝑥 ∈ 𝑅 (𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑎 ∩ 𝑐))) |
21 | | basis2 22082 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑆 ∈ TopBases ∧ 𝑏 ∈ 𝑆) ∧ (𝑑 ∈ 𝑆 ∧ 𝑣 ∈ (𝑏 ∩ 𝑑))) → ∃𝑦 ∈ 𝑆 (𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ (𝑏 ∩ 𝑑))) |
22 | 21 | exp43 436 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 ∈ TopBases → (𝑏 ∈ 𝑆 → (𝑑 ∈ 𝑆 → (𝑣 ∈ (𝑏 ∩ 𝑑) → ∃𝑦 ∈ 𝑆 (𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ (𝑏 ∩ 𝑑)))))) |
23 | 22 | imp42 426 |
. . . . . . . . . . . . . 14
⊢ (((𝑆 ∈ TopBases ∧ (𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) ∧ 𝑣 ∈ (𝑏 ∩ 𝑑)) → ∃𝑦 ∈ 𝑆 (𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ (𝑏 ∩ 𝑑))) |
24 | | reeanv 3294 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥 ∈
𝑅 ∃𝑦 ∈ 𝑆 ((𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑎 ∩ 𝑐)) ∧ (𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ (𝑏 ∩ 𝑑))) ↔ (∃𝑥 ∈ 𝑅 (𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑎 ∩ 𝑐)) ∧ ∃𝑦 ∈ 𝑆 (𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ (𝑏 ∩ 𝑑)))) |
25 | | opelxpi 5625 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑦) → 〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦)) |
26 | | xpss12 5603 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ⊆ (𝑎 ∩ 𝑐) ∧ 𝑦 ⊆ (𝑏 ∩ 𝑑)) → (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) |
27 | 25, 26 | anim12i 612 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑢 ∈ 𝑥 ∧ 𝑣 ∈ 𝑦) ∧ (𝑥 ⊆ (𝑎 ∩ 𝑐) ∧ 𝑦 ⊆ (𝑏 ∩ 𝑑))) → (〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
28 | 27 | an4s 656 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑎 ∩ 𝑐)) ∧ (𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ (𝑏 ∩ 𝑑))) → (〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
29 | 28 | reximi 3176 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑦 ∈
𝑆 ((𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑎 ∩ 𝑐)) ∧ (𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ (𝑏 ∩ 𝑑))) → ∃𝑦 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
30 | 29 | reximi 3176 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑥 ∈
𝑅 ∃𝑦 ∈ 𝑆 ((𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑎 ∩ 𝑐)) ∧ (𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ (𝑏 ∩ 𝑑))) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
31 | 24, 30 | sylbir 234 |
. . . . . . . . . . . . . 14
⊢
((∃𝑥 ∈
𝑅 (𝑢 ∈ 𝑥 ∧ 𝑥 ⊆ (𝑎 ∩ 𝑐)) ∧ ∃𝑦 ∈ 𝑆 (𝑣 ∈ 𝑦 ∧ 𝑦 ⊆ (𝑏 ∩ 𝑑))) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
32 | 20, 23, 31 | syl2an 595 |
. . . . . . . . . . . . 13
⊢ ((((𝑅 ∈ TopBases ∧ (𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅)) ∧ 𝑢 ∈ (𝑎 ∩ 𝑐)) ∧ ((𝑆 ∈ TopBases ∧ (𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) ∧ 𝑣 ∈ (𝑏 ∩ 𝑑))) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
33 | 32 | an4s 656 |
. . . . . . . . . . . 12
⊢ ((((𝑅 ∈ TopBases ∧ (𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆))) ∧ (𝑢 ∈ (𝑎 ∩ 𝑐) ∧ 𝑣 ∈ (𝑏 ∩ 𝑑))) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
34 | 33 | ralrimivva 3116 |
. . . . . . . . . . 11
⊢ (((𝑅 ∈ TopBases ∧ (𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆))) → ∀𝑢 ∈ (𝑎 ∩ 𝑐)∀𝑣 ∈ (𝑏 ∩ 𝑑)∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
35 | | eleq1 2827 |
. . . . . . . . . . . . . 14
⊢ (𝑝 = 〈𝑢, 𝑣〉 → (𝑝 ∈ (𝑥 × 𝑦) ↔ 〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦))) |
36 | 35 | anbi1d 629 |
. . . . . . . . . . . . 13
⊢ (𝑝 = 〈𝑢, 𝑣〉 → ((𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) ↔ (〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))))) |
37 | 36 | 2rexbidv 3230 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑢, 𝑣〉 → (∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))))) |
38 | 37 | ralxp 5747 |
. . . . . . . . . . 11
⊢
(∀𝑝 ∈
((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) ↔ ∀𝑢 ∈ (𝑎 ∩ 𝑐)∀𝑣 ∈ (𝑏 ∩ 𝑑)∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (〈𝑢, 𝑣〉 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
39 | 34, 38 | sylibr 233 |
. . . . . . . . . 10
⊢ (((𝑅 ∈ TopBases ∧ (𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅)) ∧ (𝑆 ∈ TopBases ∧ (𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆))) → ∀𝑝 ∈ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
40 | 39 | an4s 656 |
. . . . . . . . 9
⊢ (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ ((𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅) ∧ (𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆))) → ∀𝑝 ∈ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
41 | 40 | anassrs 467 |
. . . . . . . 8
⊢ ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅)) ∧ (𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → ∀𝑝 ∈ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
42 | | ineq12 4146 |
. . . . . . . . . 10
⊢ ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢 ∩ 𝑣) = ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑))) |
43 | | inxp 5738 |
. . . . . . . . . 10
⊢ ((𝑎 × 𝑏) ∩ (𝑐 × 𝑑)) = ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)) |
44 | 42, 43 | eqtrdi 2795 |
. . . . . . . . 9
⊢ ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑢 ∩ 𝑣) = ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) |
45 | 44 | sseq2d 3957 |
. . . . . . . . . . . 12
⊢ ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (𝑡 ⊆ (𝑢 ∩ 𝑣) ↔ 𝑡 ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
46 | 45 | anbi2d 628 |
. . . . . . . . . . 11
⊢ ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ((𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)) ↔ (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))))) |
47 | 46 | rexbidv 3227 |
. . . . . . . . . 10
⊢ ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)) ↔ ∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))))) |
48 | 1 | rexeqi 3345 |
. . . . . . . . . . 11
⊢
(∃𝑡 ∈
𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) ↔ ∃𝑡 ∈ ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦))(𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
49 | | fvex 6781 |
. . . . . . . . . . . . . 14
⊢
(1st ‘𝑧) ∈ V |
50 | | fvex 6781 |
. . . . . . . . . . . . . 14
⊢
(2nd ‘𝑧) ∈ V |
51 | 49, 50 | xpex 7594 |
. . . . . . . . . . . . 13
⊢
((1st ‘𝑧) × (2nd ‘𝑧)) ∈ V |
52 | 51 | rgenw 3077 |
. . . . . . . . . . . 12
⊢
∀𝑧 ∈
(𝑅 × 𝑆)((1st ‘𝑧) × (2nd
‘𝑧)) ∈
V |
53 | | vex 3434 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑥 ∈ V |
54 | | vex 3434 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
55 | 53, 54 | op1std 7827 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) |
56 | 53, 54 | op2ndd 7828 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
57 | 55, 56 | xpeq12d 5619 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((1st ‘𝑧) × (2nd
‘𝑧)) = (𝑥 × 𝑦)) |
58 | 57 | mpompt 7379 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st ‘𝑧) × (2nd
‘𝑧))) = (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) |
59 | 58 | eqcomi 2748 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦)) = (𝑧 ∈ (𝑅 × 𝑆) ↦ ((1st ‘𝑧) × (2nd
‘𝑧))) |
60 | | eleq2 2828 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = ((1st ‘𝑧) × (2nd
‘𝑧)) → (𝑝 ∈ 𝑡 ↔ 𝑝 ∈ ((1st ‘𝑧) × (2nd
‘𝑧)))) |
61 | | sseq1 3950 |
. . . . . . . . . . . . . 14
⊢ (𝑡 = ((1st ‘𝑧) × (2nd
‘𝑧)) → (𝑡 ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)) ↔ ((1st ‘𝑧) × (2nd
‘𝑧)) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
62 | 60, 61 | anbi12d 630 |
. . . . . . . . . . . . 13
⊢ (𝑡 = ((1st ‘𝑧) × (2nd
‘𝑧)) → ((𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) ↔ (𝑝 ∈ ((1st ‘𝑧) × (2nd
‘𝑧)) ∧
((1st ‘𝑧)
× (2nd ‘𝑧)) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))))) |
63 | 59, 62 | rexrnmptw 6965 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
(𝑅 × 𝑆)((1st ‘𝑧) × (2nd
‘𝑧)) ∈ V →
(∃𝑡 ∈ ran (𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦))(𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st ‘𝑧) × (2nd
‘𝑧)) ∧
((1st ‘𝑧)
× (2nd ‘𝑧)) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))))) |
64 | 52, 63 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(∃𝑡 ∈ ran
(𝑥 ∈ 𝑅, 𝑦 ∈ 𝑆 ↦ (𝑥 × 𝑦))(𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) ↔ ∃𝑧 ∈ (𝑅 × 𝑆)(𝑝 ∈ ((1st ‘𝑧) × (2nd
‘𝑧)) ∧
((1st ‘𝑧)
× (2nd ‘𝑧)) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
65 | 57 | eleq2d 2825 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝑝 ∈ ((1st ‘𝑧) × (2nd
‘𝑧)) ↔ 𝑝 ∈ (𝑥 × 𝑦))) |
66 | 57 | sseq1d 3956 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((1st ‘𝑧) × (2nd
‘𝑧)) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)) ↔ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
67 | 65, 66 | anbi12d 630 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝑝 ∈ ((1st ‘𝑧) × (2nd
‘𝑧)) ∧
((1st ‘𝑧)
× (2nd ‘𝑧)) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) ↔ (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))))) |
68 | 67 | rexxp 5748 |
. . . . . . . . . . 11
⊢
(∃𝑧 ∈
(𝑅 × 𝑆)(𝑝 ∈ ((1st ‘𝑧) × (2nd
‘𝑧)) ∧
((1st ‘𝑧)
× (2nd ‘𝑧)) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
69 | 48, 64, 68 | 3bitri 296 |
. . . . . . . . . 10
⊢
(∃𝑡 ∈
𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))) ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑)))) |
70 | 47, 69 | bitrdi 286 |
. . . . . . . . 9
⊢ ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)) ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))))) |
71 | 44, 70 | raleqbidv 3334 |
. . . . . . . 8
⊢ ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → (∀𝑝 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)) ↔ ∀𝑝 ∈ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 (𝑝 ∈ (𝑥 × 𝑦) ∧ (𝑥 × 𝑦) ⊆ ((𝑎 ∩ 𝑐) × (𝑏 ∩ 𝑑))))) |
72 | 41, 71 | syl5ibrcom 246 |
. . . . . . 7
⊢ ((((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅)) ∧ (𝑏 ∈ 𝑆 ∧ 𝑑 ∈ 𝑆)) → ((𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
73 | 72 | rexlimdvva 3224 |
. . . . . 6
⊢ (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅)) → (∃𝑏 ∈ 𝑆 ∃𝑑 ∈ 𝑆 (𝑢 = (𝑎 × 𝑏) ∧ 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
74 | 17, 73 | syl5bir 242 |
. . . . 5
⊢ (((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) ∧ (𝑎 ∈ 𝑅 ∧ 𝑐 ∈ 𝑅)) → ((∃𝑏 ∈ 𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑 ∈ 𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
75 | 74 | rexlimdvva 3224 |
. . . 4
⊢ ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) →
(∃𝑎 ∈ 𝑅 ∃𝑐 ∈ 𝑅 (∃𝑏 ∈ 𝑆 𝑢 = (𝑎 × 𝑏) ∧ ∃𝑑 ∈ 𝑆 𝑣 = (𝑐 × 𝑑)) → ∀𝑝 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
76 | 16, 75 | syl5bi 241 |
. . 3
⊢ ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → ((𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵) → ∀𝑝 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
77 | 76 | ralrimivv 3115 |
. 2
⊢ ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) →
∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑝 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣))) |
78 | 1 | txbasex 22698 |
. . 3
⊢ ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈ V) |
79 | | isbasis2g 22079 |
. . 3
⊢ (𝐵 ∈ V → (𝐵 ∈ TopBases ↔
∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑝 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
80 | 78, 79 | syl 17 |
. 2
⊢ ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → (𝐵 ∈ TopBases ↔
∀𝑢 ∈ 𝐵 ∀𝑣 ∈ 𝐵 ∀𝑝 ∈ (𝑢 ∩ 𝑣)∃𝑡 ∈ 𝐵 (𝑝 ∈ 𝑡 ∧ 𝑡 ⊆ (𝑢 ∩ 𝑣)))) |
81 | 77, 80 | mpbird 256 |
1
⊢ ((𝑅 ∈ TopBases ∧ 𝑆 ∈ TopBases) → 𝐵 ∈
TopBases) |