Step | Hyp | Ref
| Expression |
1 | | f1stres 7081 |
. . . . . . . . 9
⊢
(1st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐽 |
2 | | ffn 5958 |
. . . . . . . . 9
⊢
((1st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐽 → (1st ↾
(∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾)) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . 8
⊢
(1st ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾) |
4 | | fvco2 6183 |
. . . . . . . 8
⊢
(((1st ↾ (∪ 𝐽 × ∪ 𝐾))
Fn (∪ 𝐽 × ∪ 𝐾) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎))) |
5 | 3, 4 | mpan 702 |
. . . . . . 7
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → ((𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾)))‘𝑎) = (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎))) |
6 | 5 | adantl 481 |
. . . . . 6
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎))) |
7 | | fvres 6117 |
. . . . . . . 8
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → ((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎) = (1st ‘𝑎)) |
8 | 7 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)) = (𝐹‘(1st ‘𝑎))) |
9 | 8 | adantl 481 |
. . . . . 6
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)) = (𝐹‘(1st ‘𝑎))) |
10 | 6, 9 | eqtrd 2644 |
. . . . 5
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘(1st ‘𝑎))) |
11 | | fvres 6117 |
. . . . . 6
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎) = (2nd ‘𝑎)) |
12 | 11 | adantl 481 |
. . . . 5
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((2nd ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎) = (2nd ‘𝑎)) |
13 | 10, 12 | eqeq12d 2625 |
. . . 4
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ (((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎) ↔ (𝐹‘(1st ‘𝑎)) = (2nd
‘𝑎))) |
14 | 13 | rabbidva 3163 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)} = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ (𝐹‘(1st ‘𝑎)) = (2nd
‘𝑎)}) |
15 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 |
16 | | eqid 2610 |
. . . . . . . 8
⊢ ∪ 𝐾 =
∪ 𝐾 |
17 | 15, 16 | cnf 20860 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
18 | 17 | adantl 481 |
. . . . . 6
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
19 | | fco 5971 |
. . . . . 6
⊢ ((𝐹:∪
𝐽⟶∪ 𝐾
∧ (1st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐽) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐾) |
20 | 18, 1, 19 | sylancl 693 |
. . . . 5
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐾) |
21 | | ffn 5958 |
. . . . 5
⊢ ((𝐹 ∘ (1st ↾
(∪ 𝐽 × ∪ 𝐾))):(∪ 𝐽
× ∪ 𝐾)⟶∪ 𝐾 → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) Fn (∪ 𝐽 × ∪ 𝐾)) |
22 | 20, 21 | syl 17 |
. . . 4
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) Fn (∪ 𝐽 × ∪ 𝐾)) |
23 | | f2ndres 7082 |
. . . . 5
⊢
(2nd ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐾 |
24 | | ffn 5958 |
. . . . 5
⊢
((2nd ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐾 → (2nd ↾
(∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾)) |
25 | 23, 24 | ax-mp 5 |
. . . 4
⊢
(2nd ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾) |
26 | | fndmin 6232 |
. . . 4
⊢ (((𝐹 ∘ (1st ↾
(∪ 𝐽 × ∪ 𝐾))) Fn (∪ 𝐽
× ∪ 𝐾) ∧ (2nd ↾ (∪ 𝐽
× ∪ 𝐾)) Fn (∪ 𝐽 × ∪ 𝐾))
→ dom ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾))) ∩ (2nd
↾ (∪ 𝐽 × ∪ 𝐾))) = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)}) |
27 | 22, 25, 26 | sylancl 693 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → dom ((𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∩ (2nd ↾ (∪ 𝐽
× ∪ 𝐾))) = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)}) |
28 | | fgraphxp 36808 |
. . . 4
⊢ (𝐹:∪
𝐽⟶∪ 𝐾
→ 𝐹 = {𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) ∣ (𝐹‘(1st ‘𝑎)) = (2nd
‘𝑎)}) |
29 | 18, 28 | syl 17 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ (𝐹‘(1st ‘𝑎)) = (2nd
‘𝑎)}) |
30 | 14, 27, 29 | 3eqtr4rd 2655 |
. 2
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 = dom ((𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∩ (2nd ↾ (∪ 𝐽
× ∪ 𝐾)))) |
31 | | simpl 472 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Haus) |
32 | | cntop1 20854 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
33 | 32 | adantl 481 |
. . . . . 6
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Top) |
34 | 15 | toptopon 20548 |
. . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
35 | 33, 34 | sylib 207 |
. . . . 5
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
36 | | haustop 20945 |
. . . . . . 7
⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top) |
37 | 31, 36 | syl 17 |
. . . . . 6
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Top) |
38 | 16 | toptopon 20548 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
39 | 37, 38 | sylib 207 |
. . . . 5
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
40 | | tx1cn 21222 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐾 ∈
(TopOn‘∪ 𝐾)) → (1st ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
41 | 35, 39, 40 | syl2anc 691 |
. . . 4
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (1st ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
42 | | cnco 20880 |
. . . 4
⊢
(((1st ↾ (∪ 𝐽 × ∪ 𝐾))
∈ ((𝐽
×t 𝐾) Cn
𝐽) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
43 | 41, 42 | sylancom 698 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
44 | | tx2cn 21223 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐾 ∈
(TopOn‘∪ 𝐾)) → (2nd ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
45 | 35, 39, 44 | syl2anc 691 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (2nd ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
46 | 31, 43, 45 | hauseqlcld 21259 |
. 2
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → dom ((𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∩ (2nd ↾ (∪ 𝐽
× ∪ 𝐾))) ∈ (Clsd‘(𝐽 ×t 𝐾))) |
47 | 30, 46 | eqeltrd 2688 |
1
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (Clsd‘(𝐽 ×t 𝐾))) |