Step | Hyp | Ref
| Expression |
1 | | hauseqlcld.f |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
2 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝐽 =
∪ 𝐽 |
3 | | eqid 2610 |
. . . . . . . . . . 11
⊢ ∪ 𝐾 =
∪ 𝐾 |
4 | 2, 3 | cnf 20860 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
5 | 1, 4 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:∪ 𝐽⟶∪ 𝐾) |
6 | 5 | ffvelrnda 6267 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ ∪ 𝐽) → (𝐹‘𝑏) ∈ ∪ 𝐾) |
7 | 6 | biantrud 527 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ ∪ 𝐽) → (〈(𝐹‘𝑏), (𝐺‘𝑏)〉 ∈ I ↔ (〈(𝐹‘𝑏), (𝐺‘𝑏)〉 ∈ I ∧ (𝐹‘𝑏) ∈ ∪ 𝐾))) |
8 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝐺‘𝑏) ∈ V |
9 | 8 | ideq 5196 |
. . . . . . . 8
⊢ ((𝐹‘𝑏) I (𝐺‘𝑏) ↔ (𝐹‘𝑏) = (𝐺‘𝑏)) |
10 | | df-br 4584 |
. . . . . . . 8
⊢ ((𝐹‘𝑏) I (𝐺‘𝑏) ↔ 〈(𝐹‘𝑏), (𝐺‘𝑏)〉 ∈ I ) |
11 | 9, 10 | bitr3i 265 |
. . . . . . 7
⊢ ((𝐹‘𝑏) = (𝐺‘𝑏) ↔ 〈(𝐹‘𝑏), (𝐺‘𝑏)〉 ∈ I ) |
12 | 8 | opelres 5322 |
. . . . . . 7
⊢
(〈(𝐹‘𝑏), (𝐺‘𝑏)〉 ∈ ( I ↾ ∪ 𝐾)
↔ (〈(𝐹‘𝑏), (𝐺‘𝑏)〉 ∈ I ∧ (𝐹‘𝑏) ∈ ∪ 𝐾)) |
13 | 7, 11, 12 | 3bitr4g 302 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ ∪ 𝐽) → ((𝐹‘𝑏) = (𝐺‘𝑏) ↔ 〈(𝐹‘𝑏), (𝐺‘𝑏)〉 ∈ ( I ↾ ∪ 𝐾))) |
14 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏)) |
15 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (𝐺‘𝑎) = (𝐺‘𝑏)) |
16 | 14, 15 | opeq12d 4348 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → 〈(𝐹‘𝑎), (𝐺‘𝑎)〉 = 〈(𝐹‘𝑏), (𝐺‘𝑏)〉) |
17 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑎 ∈ ∪ 𝐽
↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) = (𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) |
18 | | opex 4859 |
. . . . . . . . 9
⊢
〈(𝐹‘𝑏), (𝐺‘𝑏)〉 ∈ V |
19 | 16, 17, 18 | fvmpt 6191 |
. . . . . . . 8
⊢ (𝑏 ∈ ∪ 𝐽
→ ((𝑎 ∈ ∪ 𝐽
↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)‘𝑏) = 〈(𝐹‘𝑏), (𝐺‘𝑏)〉) |
20 | 19 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ ∪ 𝐽) → ((𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)‘𝑏) = 〈(𝐹‘𝑏), (𝐺‘𝑏)〉) |
21 | 20 | eleq1d 2672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ ∪ 𝐽) → (((𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)‘𝑏) ∈ ( I ↾ ∪ 𝐾)
↔ 〈(𝐹‘𝑏), (𝐺‘𝑏)〉 ∈ ( I ↾ ∪ 𝐾))) |
22 | 13, 21 | bitr4d 270 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ ∪ 𝐽) → ((𝐹‘𝑏) = (𝐺‘𝑏) ↔ ((𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)‘𝑏) ∈ ( I ↾ ∪ 𝐾))) |
23 | 22 | pm5.32da 671 |
. . . 4
⊢ (𝜑 → ((𝑏 ∈ ∪ 𝐽 ∧ (𝐹‘𝑏) = (𝐺‘𝑏)) ↔ (𝑏 ∈ ∪ 𝐽 ∧ ((𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)‘𝑏) ∈ ( I ↾ ∪ 𝐾)))) |
24 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:∪
𝐽⟶∪ 𝐾
→ 𝐹 Fn ∪ 𝐽) |
25 | 5, 24 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn ∪ 𝐽) |
26 | | hauseqlcld.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) |
27 | 2, 3 | cnf 20860 |
. . . . . . . . 9
⊢ (𝐺 ∈ (𝐽 Cn 𝐾) → 𝐺:∪ 𝐽⟶∪ 𝐾) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:∪ 𝐽⟶∪ 𝐾) |
29 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐺:∪
𝐽⟶∪ 𝐾
→ 𝐺 Fn ∪ 𝐽) |
30 | 28, 29 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn ∪ 𝐽) |
31 | | fndmin 6232 |
. . . . . . 7
⊢ ((𝐹 Fn ∪
𝐽 ∧ 𝐺 Fn ∪ 𝐽) → dom (𝐹 ∩ 𝐺) = {𝑏 ∈ ∪ 𝐽 ∣ (𝐹‘𝑏) = (𝐺‘𝑏)}) |
32 | 25, 30, 31 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → dom (𝐹 ∩ 𝐺) = {𝑏 ∈ ∪ 𝐽 ∣ (𝐹‘𝑏) = (𝐺‘𝑏)}) |
33 | 32 | eleq2d 2673 |
. . . . 5
⊢ (𝜑 → (𝑏 ∈ dom (𝐹 ∩ 𝐺) ↔ 𝑏 ∈ {𝑏 ∈ ∪ 𝐽 ∣ (𝐹‘𝑏) = (𝐺‘𝑏)})) |
34 | | rabid 3095 |
. . . . 5
⊢ (𝑏 ∈ {𝑏 ∈ ∪ 𝐽 ∣ (𝐹‘𝑏) = (𝐺‘𝑏)} ↔ (𝑏 ∈ ∪ 𝐽 ∧ (𝐹‘𝑏) = (𝐺‘𝑏))) |
35 | 33, 34 | syl6bb 275 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ dom (𝐹 ∩ 𝐺) ↔ (𝑏 ∈ ∪ 𝐽 ∧ (𝐹‘𝑏) = (𝐺‘𝑏)))) |
36 | | opex 4859 |
. . . . . 6
⊢
〈(𝐹‘𝑎), (𝐺‘𝑎)〉 ∈ V |
37 | 36, 17 | fnmpti 5935 |
. . . . 5
⊢ (𝑎 ∈ ∪ 𝐽
↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) Fn ∪
𝐽 |
38 | | elpreima 6245 |
. . . . 5
⊢ ((𝑎 ∈ ∪ 𝐽
↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) Fn ∪
𝐽 → (𝑏 ∈ (◡(𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) “ ( I ↾ ∪ 𝐾))
↔ (𝑏 ∈ ∪ 𝐽
∧ ((𝑎 ∈ ∪ 𝐽
↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)‘𝑏) ∈ ( I ↾ ∪ 𝐾)))) |
39 | 37, 38 | mp1i 13 |
. . . 4
⊢ (𝜑 → (𝑏 ∈ (◡(𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) “ ( I ↾ ∪ 𝐾))
↔ (𝑏 ∈ ∪ 𝐽
∧ ((𝑎 ∈ ∪ 𝐽
↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉)‘𝑏) ∈ ( I ↾ ∪ 𝐾)))) |
40 | 23, 35, 39 | 3bitr4d 299 |
. . 3
⊢ (𝜑 → (𝑏 ∈ dom (𝐹 ∩ 𝐺) ↔ 𝑏 ∈ (◡(𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) “ ( I ↾ ∪ 𝐾)))) |
41 | 40 | eqrdv 2608 |
. 2
⊢ (𝜑 → dom (𝐹 ∩ 𝐺) = (◡(𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) “ ( I ↾ ∪ 𝐾))) |
42 | 2, 17 | txcnmpt 21237 |
. . . 4
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐺 ∈ (𝐽 Cn 𝐾)) → (𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) ∈ (𝐽 Cn (𝐾 ×t 𝐾))) |
43 | 1, 26, 42 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) ∈ (𝐽 Cn (𝐾 ×t 𝐾))) |
44 | | hauseqlcld.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈ Haus) |
45 | 3 | hausdiag 21258 |
. . . . 5
⊢ (𝐾 ∈ Haus ↔ (𝐾 ∈ Top ∧ ( I ↾
∪ 𝐾) ∈ (Clsd‘(𝐾 ×t 𝐾)))) |
46 | 45 | simprbi 479 |
. . . 4
⊢ (𝐾 ∈ Haus → ( I ↾
∪ 𝐾) ∈ (Clsd‘(𝐾 ×t 𝐾))) |
47 | 44, 46 | syl 17 |
. . 3
⊢ (𝜑 → ( I ↾ ∪ 𝐾)
∈ (Clsd‘(𝐾
×t 𝐾))) |
48 | | cnclima 20882 |
. . 3
⊢ (((𝑎 ∈ ∪ 𝐽
↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) ∈ (𝐽 Cn (𝐾 ×t 𝐾)) ∧ ( I ↾ ∪ 𝐾)
∈ (Clsd‘(𝐾
×t 𝐾)))
→ (◡(𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) “ ( I ↾ ∪ 𝐾))
∈ (Clsd‘𝐽)) |
49 | 43, 47, 48 | syl2anc 691 |
. 2
⊢ (𝜑 → (◡(𝑎 ∈ ∪ 𝐽 ↦ 〈(𝐹‘𝑎), (𝐺‘𝑎)〉) “ ( I ↾ ∪ 𝐾))
∈ (Clsd‘𝐽)) |
50 | 41, 49 | eqeltrd 2688 |
1
⊢ (𝜑 → dom (𝐹 ∩ 𝐺) ∈ (Clsd‘𝐽)) |