Step | Hyp | Ref
| Expression |
1 | | f1stres 7785 |
. . . . . . . . 9
⊢
(1st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐽 |
2 | | ffn 6545 |
. . . . . . . . 9
⊢
((1st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐽 → (1st ↾
(∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾)) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . 8
⊢
(1st ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾) |
4 | | fvco2 6808 |
. . . . . . . 8
⊢
(((1st ↾ (∪ 𝐽 × ∪ 𝐾))
Fn (∪ 𝐽 × ∪ 𝐾) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎))) |
5 | 3, 4 | mpan 690 |
. . . . . . 7
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → ((𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾)))‘𝑎) = (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎))) |
6 | 5 | adantl 485 |
. . . . . 6
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎))) |
7 | | fvres 6736 |
. . . . . . . 8
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → ((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎) = (1st ‘𝑎)) |
8 | 7 | fveq2d 6721 |
. . . . . . 7
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)) = (𝐹‘(1st ‘𝑎))) |
9 | 8 | adantl 485 |
. . . . . 6
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)) = (𝐹‘(1st ‘𝑎))) |
10 | 6, 9 | eqtrd 2777 |
. . . . 5
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘(1st ‘𝑎))) |
11 | | fvres 6736 |
. . . . . 6
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎) = (2nd ‘𝑎)) |
12 | 11 | adantl 485 |
. . . . 5
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((2nd ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎) = (2nd ‘𝑎)) |
13 | 10, 12 | eqeq12d 2753 |
. . . 4
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ (((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎) ↔ (𝐹‘(1st ‘𝑎)) = (2nd
‘𝑎))) |
14 | 13 | rabbidva 3388 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)} = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ (𝐹‘(1st ‘𝑎)) = (2nd
‘𝑎)}) |
15 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 |
16 | | eqid 2737 |
. . . . . . . 8
⊢ ∪ 𝐾 =
∪ 𝐾 |
17 | 15, 16 | cnf 22143 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
18 | 17 | adantl 485 |
. . . . . 6
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:∪ 𝐽⟶∪ 𝐾) |
19 | | fco 6569 |
. . . . . 6
⊢ ((𝐹:∪
𝐽⟶∪ 𝐾
∧ (1st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐽) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐾) |
20 | 18, 1, 19 | sylancl 589 |
. . . . 5
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐾) |
21 | 20 | ffnd 6546 |
. . . 4
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) Fn (∪ 𝐽 × ∪ 𝐾)) |
22 | | f2ndres 7786 |
. . . . 5
⊢
(2nd ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐾 |
23 | | ffn 6545 |
. . . . 5
⊢
((2nd ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐾 → (2nd ↾
(∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾)) |
24 | 22, 23 | ax-mp 5 |
. . . 4
⊢
(2nd ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾) |
25 | | fndmin 6865 |
. . . 4
⊢ (((𝐹 ∘ (1st ↾
(∪ 𝐽 × ∪ 𝐾))) Fn (∪ 𝐽
× ∪ 𝐾) ∧ (2nd ↾ (∪ 𝐽
× ∪ 𝐾)) Fn (∪ 𝐽 × ∪ 𝐾))
→ dom ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾))) ∩ (2nd
↾ (∪ 𝐽 × ∪ 𝐾))) = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)}) |
26 | 21, 24, 25 | sylancl 589 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → dom ((𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∩ (2nd ↾ (∪ 𝐽
× ∪ 𝐾))) = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)}) |
27 | | fgraphxp 40739 |
. . . 4
⊢ (𝐹:∪
𝐽⟶∪ 𝐾
→ 𝐹 = {𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) ∣ (𝐹‘(1st ‘𝑎)) = (2nd
‘𝑎)}) |
28 | 18, 27 | syl 17 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ (𝐹‘(1st ‘𝑎)) = (2nd
‘𝑎)}) |
29 | 14, 26, 28 | 3eqtr4rd 2788 |
. 2
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 = dom ((𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∩ (2nd ↾ (∪ 𝐽
× ∪ 𝐾)))) |
30 | | simpl 486 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Haus) |
31 | | cntop1 22137 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
32 | 31 | adantl 485 |
. . . . . 6
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Top) |
33 | 15 | toptopon 21814 |
. . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
34 | 32, 33 | sylib 221 |
. . . . 5
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
35 | | haustop 22228 |
. . . . . . 7
⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top) |
36 | 30, 35 | syl 17 |
. . . . . 6
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Top) |
37 | 16 | toptopon 21814 |
. . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) |
38 | 36, 37 | sylib 221 |
. . . . 5
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ (TopOn‘∪ 𝐾)) |
39 | | tx1cn 22506 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐾 ∈
(TopOn‘∪ 𝐾)) → (1st ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
40 | 34, 38, 39 | syl2anc 587 |
. . . 4
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (1st ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) |
41 | | cnco 22163 |
. . . 4
⊢
(((1st ↾ (∪ 𝐽 × ∪ 𝐾))
∈ ((𝐽
×t 𝐾) Cn
𝐽) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
42 | 40, 41 | sylancom 591 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
43 | | tx2cn 22507 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐾 ∈
(TopOn‘∪ 𝐾)) → (2nd ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
44 | 34, 38, 43 | syl2anc 587 |
. . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (2nd ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) |
45 | 30, 42, 44 | hauseqlcld 22543 |
. 2
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → dom ((𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∩ (2nd ↾ (∪ 𝐽
× ∪ 𝐾))) ∈ (Clsd‘(𝐽 ×t 𝐾))) |
46 | 29, 45 | eqeltrd 2838 |
1
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (Clsd‘(𝐽 ×t 𝐾))) |