Step | Hyp | Ref
| Expression |
1 | | paste.7 |
. 2
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
2 | | paste.6 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝑋) |
3 | 2 | ineq2d 4139 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ 𝑦) ∩ (𝐴 ∪ 𝐵)) = ((◡𝐹 “ 𝑦) ∩ 𝑋)) |
4 | | indi 4200 |
. . . . . . 7
⊢ ((◡𝐹 “ 𝑦) ∩ (𝐴 ∪ 𝐵)) = (((◡𝐹 “ 𝑦) ∩ 𝐴) ∪ ((◡𝐹 “ 𝑦) ∩ 𝐵)) |
5 | 1 | ffund 6491 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐹) |
6 | | respreima 6813 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (◡(𝐹 ↾ 𝐴) “ 𝑦) = ((◡𝐹 “ 𝑦) ∩ 𝐴)) |
7 | | respreima 6813 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝑦) = ((◡𝐹 “ 𝑦) ∩ 𝐵)) |
8 | 6, 7 | uneq12d 4091 |
. . . . . . . 8
⊢ (Fun
𝐹 → ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦)) = (((◡𝐹 “ 𝑦) ∩ 𝐴) ∪ ((◡𝐹 “ 𝑦) ∩ 𝐵))) |
9 | 5, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦)) = (((◡𝐹 “ 𝑦) ∩ 𝐴) ∪ ((◡𝐹 “ 𝑦) ∩ 𝐵))) |
10 | 4, 9 | eqtr4id 2852 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ 𝑦) ∩ (𝐴 ∪ 𝐵)) = ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦))) |
11 | | imassrn 5907 |
. . . . . . . . 9
⊢ (◡𝐹 “ 𝑦) ⊆ ran ◡𝐹 |
12 | | dfdm4 5728 |
. . . . . . . . . 10
⊢ dom 𝐹 = ran ◡𝐹 |
13 | | fdm 6495 |
. . . . . . . . . 10
⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋) |
14 | 12, 13 | syl5eqr 2847 |
. . . . . . . . 9
⊢ (𝐹:𝑋⟶𝑌 → ran ◡𝐹 = 𝑋) |
15 | 11, 14 | sseqtrid 3967 |
. . . . . . . 8
⊢ (𝐹:𝑋⟶𝑌 → (◡𝐹 “ 𝑦) ⊆ 𝑋) |
16 | 1, 15 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (◡𝐹 “ 𝑦) ⊆ 𝑋) |
17 | | df-ss 3898 |
. . . . . . 7
⊢ ((◡𝐹 “ 𝑦) ⊆ 𝑋 ↔ ((◡𝐹 “ 𝑦) ∩ 𝑋) = (◡𝐹 “ 𝑦)) |
18 | 16, 17 | sylib 221 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ 𝑦) ∩ 𝑋) = (◡𝐹 “ 𝑦)) |
19 | 3, 10, 18 | 3eqtr3rd 2842 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ 𝑦) = ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦))) |
20 | 19 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝑦) = ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦))) |
21 | | paste.4 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽)) |
22 | | paste.8 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) |
23 | | cnclima 21873 |
. . . . . . 7
⊢ (((𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐴))) |
24 | 22, 23 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐴))) |
25 | | restcldr 21779 |
. . . . . 6
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ (◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐴))) → (◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘𝐽)) |
26 | 21, 24, 25 | syl2an2r 684 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘𝐽)) |
27 | | paste.5 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽)) |
28 | | paste.9 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ ((𝐽 ↾t 𝐵) Cn 𝐾)) |
29 | | cnclima 21873 |
. . . . . . 7
⊢ (((𝐹 ↾ 𝐵) ∈ ((𝐽 ↾t 𝐵) Cn 𝐾) ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐵))) |
30 | 28, 29 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐵))) |
31 | | restcldr 21779 |
. . . . . 6
⊢ ((𝐵 ∈ (Clsd‘𝐽) ∧ (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐵))) → (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘𝐽)) |
32 | 27, 30, 31 | syl2an2r 684 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘𝐽)) |
33 | | uncld 21646 |
. . . . 5
⊢ (((◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘𝐽) ∧ (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘𝐽)) → ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦)) ∈ (Clsd‘𝐽)) |
34 | 26, 32, 33 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦)) ∈ (Clsd‘𝐽)) |
35 | 20, 34 | eqeltrd 2890 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)) |
36 | 35 | ralrimiva 3149 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ (Clsd‘𝐾)(◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)) |
37 | | cldrcl 21631 |
. . . 4
⊢ (𝐴 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) |
38 | 21, 37 | syl 17 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
39 | | cntop2 21846 |
. . . 4
⊢ ((𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) → 𝐾 ∈ Top) |
40 | 22, 39 | syl 17 |
. . 3
⊢ (𝜑 → 𝐾 ∈ Top) |
41 | | paste.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
42 | 41 | toptopon 21522 |
. . . 4
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
43 | | paste.2 |
. . . . 5
⊢ 𝑌 = ∪
𝐾 |
44 | 43 | toptopon 21522 |
. . . 4
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
45 | | iscncl 21874 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)))) |
46 | 42, 44, 45 | syl2anb 600 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)))) |
47 | 38, 40, 46 | syl2anc 587 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)))) |
48 | 1, 36, 47 | mpbir2and 712 |
1
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |