| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | f1stres 8038 | . . . . . . . . 9
⊢
(1st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐽 | 
| 2 |  | ffn 6736 | . . . . . . . . 9
⊢
((1st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐽 → (1st ↾
(∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾)) | 
| 3 | 1, 2 | ax-mp 5 | . . . . . . . 8
⊢
(1st ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾) | 
| 4 |  | fvco2 7006 | . . . . . . . 8
⊢
(((1st ↾ (∪ 𝐽 × ∪ 𝐾))
Fn (∪ 𝐽 × ∪ 𝐾) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎))) | 
| 5 | 3, 4 | mpan 690 | . . . . . . 7
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → ((𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾)))‘𝑎) = (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎))) | 
| 6 | 5 | adantl 481 | . . . . . 6
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎))) | 
| 7 |  | fvres 6925 | . . . . . . . 8
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → ((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎) = (1st ‘𝑎)) | 
| 8 | 7 | fveq2d 6910 | . . . . . . 7
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)) = (𝐹‘(1st ‘𝑎))) | 
| 9 | 8 | adantl 481 | . . . . . 6
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ (𝐹‘((1st ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)) = (𝐹‘(1st ‘𝑎))) | 
| 10 | 6, 9 | eqtrd 2777 | . . . . 5
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = (𝐹‘(1st ‘𝑎))) | 
| 11 |  | fvres 6925 | . . . . . 6
⊢ (𝑎 ∈ (∪ 𝐽
× ∪ 𝐾) → ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎) = (2nd ‘𝑎)) | 
| 12 | 11 | adantl 481 | . . . . 5
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ ((2nd ↾ (∪ 𝐽 × ∪ 𝐾))‘𝑎) = (2nd ‘𝑎)) | 
| 13 | 10, 12 | eqeq12d 2753 | . . . 4
⊢ (((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) ∧ 𝑎 ∈ (∪ 𝐽 × ∪ 𝐾))
→ (((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎) ↔ (𝐹‘(1st ‘𝑎)) = (2nd
‘𝑎))) | 
| 14 | 13 | rabbidva 3443 | . . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)} = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ (𝐹‘(1st ‘𝑎)) = (2nd
‘𝑎)}) | 
| 15 |  | eqid 2737 | . . . . . . . 8
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 16 |  | eqid 2737 | . . . . . . . 8
⊢ ∪ 𝐾 =
∪ 𝐾 | 
| 17 | 15, 16 | cnf 23254 | . . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:∪ 𝐽⟶∪ 𝐾) | 
| 18 | 17 | adantl 481 | . . . . . 6
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:∪ 𝐽⟶∪ 𝐾) | 
| 19 |  | fco 6760 | . . . . . 6
⊢ ((𝐹:∪
𝐽⟶∪ 𝐾
∧ (1st ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐽) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐾) | 
| 20 | 18, 1, 19 | sylancl 586 | . . . . 5
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))):(∪ 𝐽 × ∪ 𝐾)⟶∪ 𝐾) | 
| 21 | 20 | ffnd 6737 | . . . 4
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) Fn (∪ 𝐽 × ∪ 𝐾)) | 
| 22 |  | f2ndres 8039 | . . . . 5
⊢
(2nd ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐾 | 
| 23 |  | ffn 6736 | . . . . 5
⊢
((2nd ↾ (∪ 𝐽 × ∪ 𝐾)):(∪
𝐽 × ∪ 𝐾)⟶∪ 𝐾 → (2nd ↾
(∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾)) | 
| 24 | 22, 23 | ax-mp 5 | . . . 4
⊢
(2nd ↾ (∪ 𝐽 × ∪ 𝐾)) Fn (∪ 𝐽
× ∪ 𝐾) | 
| 25 |  | fndmin 7065 | . . . 4
⊢ (((𝐹 ∘ (1st ↾
(∪ 𝐽 × ∪ 𝐾))) Fn (∪ 𝐽
× ∪ 𝐾) ∧ (2nd ↾ (∪ 𝐽
× ∪ 𝐾)) Fn (∪ 𝐽 × ∪ 𝐾))
→ dom ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾))) ∩ (2nd
↾ (∪ 𝐽 × ∪ 𝐾))) = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)}) | 
| 26 | 21, 24, 25 | sylancl 586 | . . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → dom ((𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∩ (2nd ↾ (∪ 𝐽
× ∪ 𝐾))) = {𝑎 ∈ (∪ 𝐽 × ∪ 𝐾)
∣ ((𝐹 ∘
(1st ↾ (∪ 𝐽 × ∪ 𝐾)))‘𝑎) = ((2nd ↾ (∪ 𝐽
× ∪ 𝐾))‘𝑎)}) | 
| 27 |  | fgraphxp 43216 | . . . 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 482 | . . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Haus) | 
| 31 |  | cntop1 23248 | . . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) | 
| 32 | 31 | adantl 481 | . . . . . 6
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ Top) | 
| 33 | 15 | toptopon 22923 | . . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) | 
| 34 | 32, 33 | sylib 218 | . . . . 5
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐽 ∈ (TopOn‘∪ 𝐽)) | 
| 35 |  | haustop 23339 | . . . . . . 7
⊢ (𝐾 ∈ Haus → 𝐾 ∈ Top) | 
| 36 | 30, 35 | syl 17 | . . . . . 6
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ Top) | 
| 37 | 16 | toptopon 22923 | . . . . . 6
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘∪ 𝐾)) | 
| 38 | 36, 37 | sylib 218 | . . . . 5
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐾 ∈ (TopOn‘∪ 𝐾)) | 
| 39 |  | tx1cn 23617 | . . . . 5
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐾 ∈
(TopOn‘∪ 𝐾)) → (1st ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) | 
| 40 | 34, 38, 39 | syl2anc 584 | . . . 4
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (1st ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐽)) | 
| 41 |  | cnco 23274 | . . . 4
⊢
(((1st ↾ (∪ 𝐽 × ∪ 𝐾))
∈ ((𝐽
×t 𝐾) Cn
𝐽) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) | 
| 42 | 40, 41 | sylancom 588 | . . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) | 
| 43 |  | tx2cn 23618 | . . . 4
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐾 ∈
(TopOn‘∪ 𝐾)) → (2nd ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) | 
| 44 | 34, 38, 43 | syl2anc 584 | . . 3
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (2nd ↾ (∪ 𝐽
× ∪ 𝐾)) ∈ ((𝐽 ×t 𝐾) Cn 𝐾)) | 
| 45 | 30, 42, 44 | hauseqlcld 23654 | . 2
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → dom ((𝐹 ∘ (1st ↾ (∪ 𝐽
× ∪ 𝐾))) ∩ (2nd ↾ (∪ 𝐽
× ∪ 𝐾))) ∈ (Clsd‘(𝐽 ×t 𝐾))) | 
| 46 | 29, 45 | eqeltrd 2841 | 1
⊢ ((𝐾 ∈ Haus ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹 ∈ (Clsd‘(𝐽 ×t 𝐾))) |