Proof of Theorem hauseqcn
| Step | Hyp | Ref
| Expression |
| 1 | | hauseqcn.x |
. . 3
⊢ 𝑋 = ∪
𝐽 |
| 2 | | hauseqcn.f |
. . . . . 6
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
| 3 | | cntop1 23248 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
| 4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Top) |
| 5 | | dmin 5922 |
. . . . . 6
⊢ dom
(𝐹 ∩ 𝐺) ⊆ (dom 𝐹 ∩ dom 𝐺) |
| 6 | | eqid 2737 |
. . . . . . . . . 10
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 7 | | eqid 2737 |
. . . . . . . . . 10
⊢ ∪ 𝐾 =
∪ 𝐾 |
| 8 | 6, 7 | cnf 23254 |
. . . . . . . . 9
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
| 9 | | fdm 6745 |
. . . . . . . . 9
⊢ (𝐹:∪
𝐽⟶∪ 𝐾
→ dom 𝐹 = ∪ 𝐽) |
| 10 | 2, 8, 9 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐹 = ∪ 𝐽) |
| 11 | | hauseqcn.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn 𝐾)) |
| 12 | 6, 7 | cnf 23254 |
. . . . . . . . 9
⊢ (𝐺 ∈ (𝐽 Cn 𝐾) → 𝐺:∪ 𝐽⟶∪ 𝐾) |
| 13 | | fdm 6745 |
. . . . . . . . 9
⊢ (𝐺:∪
𝐽⟶∪ 𝐾
→ dom 𝐺 = ∪ 𝐽) |
| 14 | 11, 12, 13 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐺 = ∪ 𝐽) |
| 15 | 10, 14 | ineq12d 4221 |
. . . . . . 7
⊢ (𝜑 → (dom 𝐹 ∩ dom 𝐺) = (∪ 𝐽 ∩ ∪ 𝐽)) |
| 16 | | inidm 4227 |
. . . . . . 7
⊢ (∪ 𝐽
∩ ∪ 𝐽) = ∪ 𝐽 |
| 17 | 15, 16 | eqtrdi 2793 |
. . . . . 6
⊢ (𝜑 → (dom 𝐹 ∩ dom 𝐺) = ∪ 𝐽) |
| 18 | 5, 17 | sseqtrid 4026 |
. . . . 5
⊢ (𝜑 → dom (𝐹 ∩ 𝐺) ⊆ ∪ 𝐽) |
| 19 | | hauseqcn.e |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴)) |
| 20 | | ffn 6736 |
. . . . . . . 8
⊢ (𝐹:∪
𝐽⟶∪ 𝐾
→ 𝐹 Fn ∪ 𝐽) |
| 21 | 2, 8, 20 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn ∪ 𝐽) |
| 22 | | ffn 6736 |
. . . . . . . 8
⊢ (𝐺:∪
𝐽⟶∪ 𝐾
→ 𝐺 Fn ∪ 𝐽) |
| 23 | 11, 12, 22 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn ∪ 𝐽) |
| 24 | | hauseqcn.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ⊆ 𝑋) |
| 25 | 24, 1 | sseqtrdi 4024 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ ∪ 𝐽) |
| 26 | | fnreseql 7068 |
. . . . . . 7
⊢ ((𝐹 Fn ∪
𝐽 ∧ 𝐺 Fn ∪ 𝐽 ∧ 𝐴 ⊆ ∪ 𝐽) → ((𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴) ↔ 𝐴 ⊆ dom (𝐹 ∩ 𝐺))) |
| 27 | 21, 23, 25, 26 | syl3anc 1373 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ↾ 𝐴) = (𝐺 ↾ 𝐴) ↔ 𝐴 ⊆ dom (𝐹 ∩ 𝐺))) |
| 28 | 19, 27 | mpbid 232 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ dom (𝐹 ∩ 𝐺)) |
| 29 | 6 | clsss 23062 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ dom (𝐹 ∩ 𝐺) ⊆ ∪ 𝐽 ∧ 𝐴 ⊆ dom (𝐹 ∩ 𝐺)) → ((cls‘𝐽)‘𝐴) ⊆ ((cls‘𝐽)‘dom (𝐹 ∩ 𝐺))) |
| 30 | 4, 18, 28, 29 | syl3anc 1373 |
. . . 4
⊢ (𝜑 → ((cls‘𝐽)‘𝐴) ⊆ ((cls‘𝐽)‘dom (𝐹 ∩ 𝐺))) |
| 31 | | hauseqcn.c |
. . . 4
⊢ (𝜑 → ((cls‘𝐽)‘𝐴) = 𝑋) |
| 32 | | hauseqcn.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ Haus) |
| 33 | 32, 2, 11 | hauseqlcld 23654 |
. . . . 5
⊢ (𝜑 → dom (𝐹 ∩ 𝐺) ∈ (Clsd‘𝐽)) |
| 34 | | cldcls 23050 |
. . . . 5
⊢ (dom
(𝐹 ∩ 𝐺) ∈ (Clsd‘𝐽) → ((cls‘𝐽)‘dom (𝐹 ∩ 𝐺)) = dom (𝐹 ∩ 𝐺)) |
| 35 | 33, 34 | syl 17 |
. . . 4
⊢ (𝜑 → ((cls‘𝐽)‘dom (𝐹 ∩ 𝐺)) = dom (𝐹 ∩ 𝐺)) |
| 36 | 30, 31, 35 | 3sstr3d 4038 |
. . 3
⊢ (𝜑 → 𝑋 ⊆ dom (𝐹 ∩ 𝐺)) |
| 37 | 1, 36 | eqsstrrid 4023 |
. 2
⊢ (𝜑 → ∪ 𝐽
⊆ dom (𝐹 ∩ 𝐺)) |
| 38 | | fneqeql2 7067 |
. . 3
⊢ ((𝐹 Fn ∪
𝐽 ∧ 𝐺 Fn ∪ 𝐽) → (𝐹 = 𝐺 ↔ ∪ 𝐽 ⊆ dom (𝐹 ∩ 𝐺))) |
| 39 | 21, 23, 38 | syl2anc 584 |
. 2
⊢ (𝜑 → (𝐹 = 𝐺 ↔ ∪ 𝐽 ⊆ dom (𝐹 ∩ 𝐺))) |
| 40 | 37, 39 | mpbird 257 |
1
⊢ (𝜑 → 𝐹 = 𝐺) |