Step | Hyp | Ref
| Expression |
1 | | iooex 12069 |
. . . 4
⊢ (,)
∈ V |
2 | 1 | rnex 6992 |
. . 3
⊢ ran (,)
∈ V |
3 | | imassrn 5396 |
. . 3
⊢ ((,)
“ (𝑆 × 𝑆)) ⊆ ran
(,) |
4 | 2, 3 | ssexi 4731 |
. 2
⊢ ((,)
“ (𝑆 × 𝑆)) ∈ V |
5 | | qtopbas.1 |
. . . . . . . . 9
⊢ 𝑆 ⊆
ℝ* |
6 | 5 | sseli 3564 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝑆 → 𝑧 ∈ ℝ*) |
7 | 5 | sseli 3564 |
. . . . . . . 8
⊢ (𝑤 ∈ 𝑆 → 𝑤 ∈ ℝ*) |
8 | 6, 7 | anim12i 588 |
. . . . . . 7
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → (𝑧 ∈ ℝ* ∧ 𝑤 ∈
ℝ*)) |
9 | 5 | sseli 3564 |
. . . . . . . 8
⊢ (𝑣 ∈ 𝑆 → 𝑣 ∈ ℝ*) |
10 | 5 | sseli 3564 |
. . . . . . . 8
⊢ (𝑢 ∈ 𝑆 → 𝑢 ∈ ℝ*) |
11 | 9, 10 | anim12i 588 |
. . . . . . 7
⊢ ((𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → (𝑣 ∈ ℝ* ∧ 𝑢 ∈
ℝ*)) |
12 | | iooin 12080 |
. . . . . . 7
⊢ (((𝑧 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) ∧ (𝑣 ∈ ℝ* ∧ 𝑢 ∈ ℝ*))
→ ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) = (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢))) |
13 | 8, 11, 12 | syl2an 493 |
. . . . . 6
⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) = (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢))) |
14 | | ifcl 4080 |
. . . . . . . . 9
⊢ ((𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆) → if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆) |
15 | 14 | ancoms 468 |
. . . . . . . 8
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) → if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆) |
16 | | ifcl 4080 |
. . . . . . . 8
⊢ ((𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆) → if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) |
17 | | df-ov 6552 |
. . . . . . . . 9
⊢ (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) = ((,)‘〈if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)〉) |
18 | | opelxpi 5072 |
. . . . . . . . . 10
⊢
((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → 〈if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)〉 ∈ (𝑆 × 𝑆)) |
19 | | ioof 12142 |
. . . . . . . . . . . 12
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
20 | | ffun 5961 |
. . . . . . . . . . . 12
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → Fun (,)) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . 11
⊢ Fun
(,) |
22 | | xpss12 5148 |
. . . . . . . . . . . . 13
⊢ ((𝑆 ⊆ ℝ*
∧ 𝑆 ⊆
ℝ*) → (𝑆 × 𝑆) ⊆ (ℝ* ×
ℝ*)) |
23 | 5, 5, 22 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑆 × 𝑆) ⊆ (ℝ* ×
ℝ*) |
24 | 19 | fdmi 5965 |
. . . . . . . . . . . 12
⊢ dom (,) =
(ℝ* × ℝ*) |
25 | 23, 24 | sseqtr4i 3601 |
. . . . . . . . . . 11
⊢ (𝑆 × 𝑆) ⊆ dom (,) |
26 | | funfvima2 6397 |
. . . . . . . . . . 11
⊢ ((Fun (,)
∧ (𝑆 × 𝑆) ⊆ dom (,)) →
(〈if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)〉 ∈ (𝑆 × 𝑆) → ((,)‘〈if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)〉) ∈ ((,) “ (𝑆 × 𝑆)))) |
27 | 21, 25, 26 | mp2an 704 |
. . . . . . . . . 10
⊢
(〈if(𝑧 ≤
𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)〉 ∈ (𝑆 × 𝑆) → ((,)‘〈if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)〉) ∈ ((,) “ (𝑆 × 𝑆))) |
28 | 18, 27 | syl 17 |
. . . . . . . . 9
⊢
((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → ((,)‘〈if(𝑧 ≤ 𝑣, 𝑣, 𝑧), if(𝑤 ≤ 𝑢, 𝑤, 𝑢)〉) ∈ ((,) “ (𝑆 × 𝑆))) |
29 | 17, 28 | syl5eqel 2692 |
. . . . . . . 8
⊢
((if(𝑧 ≤ 𝑣, 𝑣, 𝑧) ∈ 𝑆 ∧ if(𝑤 ≤ 𝑢, 𝑤, 𝑢) ∈ 𝑆) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆))) |
30 | 15, 16, 29 | syl2an 493 |
. . . . . . 7
⊢ (((𝑧 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆) ∧ (𝑤 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆))) |
31 | 30 | an4s 865 |
. . . . . 6
⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → (if(𝑧 ≤ 𝑣, 𝑣, 𝑧)(,)if(𝑤 ≤ 𝑢, 𝑤, 𝑢)) ∈ ((,) “ (𝑆 × 𝑆))) |
32 | 13, 31 | eqeltrd 2688 |
. . . . 5
⊢ (((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) ∧ (𝑣 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆)) → ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))) |
33 | 32 | ralrimivva 2954 |
. . . 4
⊢ ((𝑧 ∈ 𝑆 ∧ 𝑤 ∈ 𝑆) → ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))) |
34 | 33 | rgen2a 2960 |
. . 3
⊢
∀𝑧 ∈
𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)) |
35 | | ffn 5958 |
. . . . . 6
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
36 | 19, 35 | ax-mp 5 |
. . . . 5
⊢ (,) Fn
(ℝ* × ℝ*) |
37 | | ineq1 3769 |
. . . . . . . 8
⊢ (𝑥 = ((,)‘𝑡) → (𝑥 ∩ 𝑦) = (((,)‘𝑡) ∩ 𝑦)) |
38 | 37 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑥 = ((,)‘𝑡) → ((𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ (((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)))) |
39 | 38 | ralbidv 2969 |
. . . . . 6
⊢ (𝑥 = ((,)‘𝑡) → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)))) |
40 | 39 | ralima 6402 |
. . . . 5
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ (𝑆 × 𝑆) ⊆ (ℝ* ×
ℝ*)) → (∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)))) |
41 | 36, 23, 40 | mp2an 704 |
. . . 4
⊢
(∀𝑥 ∈
((,) “ (𝑆 ×
𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))) |
42 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑡 = 〈𝑧, 𝑤〉 → ((,)‘𝑡) = ((,)‘〈𝑧, 𝑤〉)) |
43 | | df-ov 6552 |
. . . . . . . . . 10
⊢ (𝑧(,)𝑤) = ((,)‘〈𝑧, 𝑤〉) |
44 | 42, 43 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑡 = 〈𝑧, 𝑤〉 → ((,)‘𝑡) = (𝑧(,)𝑤)) |
45 | 44 | ineq1d 3775 |
. . . . . . . 8
⊢ (𝑡 = 〈𝑧, 𝑤〉 → (((,)‘𝑡) ∩ 𝑦) = ((𝑧(,)𝑤) ∩ 𝑦)) |
46 | 45 | eleq1d 2672 |
. . . . . . 7
⊢ (𝑡 = 〈𝑧, 𝑤〉 → ((((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)))) |
47 | 46 | ralbidv 2969 |
. . . . . 6
⊢ (𝑡 = 〈𝑧, 𝑤〉 → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)))) |
48 | | ineq2 3770 |
. . . . . . . . . 10
⊢ (𝑦 = ((,)‘𝑡) → ((𝑧(,)𝑤) ∩ 𝑦) = ((𝑧(,)𝑤) ∩ ((,)‘𝑡))) |
49 | 48 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑦 = ((,)‘𝑡) → (((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)))) |
50 | 49 | ralima 6402 |
. . . . . . . 8
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ (𝑆 × 𝑆) ⊆ (ℝ* ×
ℝ*)) → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)))) |
51 | 36, 23, 50 | mp2an 704 |
. . . . . . 7
⊢
(∀𝑦 ∈
((,) “ (𝑆 ×
𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑡 ∈ (𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆))) |
52 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑡 = 〈𝑣, 𝑢〉 → ((,)‘𝑡) = ((,)‘〈𝑣, 𝑢〉)) |
53 | | df-ov 6552 |
. . . . . . . . . . 11
⊢ (𝑣(,)𝑢) = ((,)‘〈𝑣, 𝑢〉) |
54 | 52, 53 | syl6eqr 2662 |
. . . . . . . . . 10
⊢ (𝑡 = 〈𝑣, 𝑢〉 → ((,)‘𝑡) = (𝑣(,)𝑢)) |
55 | 54 | ineq2d 3776 |
. . . . . . . . 9
⊢ (𝑡 = 〈𝑣, 𝑢〉 → ((𝑧(,)𝑤) ∩ ((,)‘𝑡)) = ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢))) |
56 | 55 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑡 = 〈𝑣, 𝑢〉 → (((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))) |
57 | 56 | ralxp 5185 |
. . . . . . 7
⊢
(∀𝑡 ∈
(𝑆 × 𝑆)((𝑧(,)𝑤) ∩ ((,)‘𝑡)) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))) |
58 | 51, 57 | bitri 263 |
. . . . . 6
⊢
(∀𝑦 ∈
((,) “ (𝑆 ×
𝑆))((𝑧(,)𝑤) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))) |
59 | 47, 58 | syl6bb 275 |
. . . . 5
⊢ (𝑡 = 〈𝑧, 𝑤〉 → (∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆)))) |
60 | 59 | ralxp 5185 |
. . . 4
⊢
(∀𝑡 ∈
(𝑆 × 𝑆)∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(((,)‘𝑡) ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))) |
61 | 41, 60 | bitri 263 |
. . 3
⊢
(∀𝑥 ∈
((,) “ (𝑆 ×
𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) ↔ ∀𝑧 ∈ 𝑆 ∀𝑤 ∈ 𝑆 ∀𝑣 ∈ 𝑆 ∀𝑢 ∈ 𝑆 ((𝑧(,)𝑤) ∩ (𝑣(,)𝑢)) ∈ ((,) “ (𝑆 × 𝑆))) |
62 | 34, 61 | mpbir 220 |
. 2
⊢
∀𝑥 ∈
((,) “ (𝑆 ×
𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆)) |
63 | | fiinbas 20567 |
. 2
⊢ ((((,)
“ (𝑆 × 𝑆)) ∈ V ∧ ∀𝑥 ∈ ((,) “ (𝑆 × 𝑆))∀𝑦 ∈ ((,) “ (𝑆 × 𝑆))(𝑥 ∩ 𝑦) ∈ ((,) “ (𝑆 × 𝑆))) → ((,) “ (𝑆 × 𝑆)) ∈ TopBases) |
64 | 4, 62, 63 | mp2an 704 |
1
⊢ ((,)
“ (𝑆 × 𝑆)) ∈
TopBases |