Step | Hyp | Ref
| Expression |
1 | | paste.7 |
. 2
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
2 | | paste.6 |
. . . . . . 7
⊢ (𝜑 → (𝐴 ∪ 𝐵) = 𝑋) |
3 | 2 | ineq2d 3814 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ 𝑦) ∩ (𝐴 ∪ 𝐵)) = ((◡𝐹 “ 𝑦) ∩ 𝑋)) |
4 | | ffun 6048 |
. . . . . . . . 9
⊢ (𝐹:𝑋⟶𝑌 → Fun 𝐹) |
5 | 1, 4 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐹) |
6 | | respreima 6344 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (◡(𝐹 ↾ 𝐴) “ 𝑦) = ((◡𝐹 “ 𝑦) ∩ 𝐴)) |
7 | | respreima 6344 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (◡(𝐹 ↾ 𝐵) “ 𝑦) = ((◡𝐹 “ 𝑦) ∩ 𝐵)) |
8 | 6, 7 | uneq12d 3768 |
. . . . . . . 8
⊢ (Fun
𝐹 → ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦)) = (((◡𝐹 “ 𝑦) ∩ 𝐴) ∪ ((◡𝐹 “ 𝑦) ∩ 𝐵))) |
9 | 5, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦)) = (((◡𝐹 “ 𝑦) ∩ 𝐴) ∪ ((◡𝐹 “ 𝑦) ∩ 𝐵))) |
10 | | indi 3873 |
. . . . . . 7
⊢ ((◡𝐹 “ 𝑦) ∩ (𝐴 ∪ 𝐵)) = (((◡𝐹 “ 𝑦) ∩ 𝐴) ∪ ((◡𝐹 “ 𝑦) ∩ 𝐵)) |
11 | 9, 10 | syl6reqr 2675 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ 𝑦) ∩ (𝐴 ∪ 𝐵)) = ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦))) |
12 | | imassrn 5477 |
. . . . . . . . 9
⊢ (◡𝐹 “ 𝑦) ⊆ ran ◡𝐹 |
13 | | dfdm4 5316 |
. . . . . . . . . 10
⊢ dom 𝐹 = ran ◡𝐹 |
14 | | fdm 6051 |
. . . . . . . . . 10
⊢ (𝐹:𝑋⟶𝑌 → dom 𝐹 = 𝑋) |
15 | 13, 14 | syl5eqr 2670 |
. . . . . . . . 9
⊢ (𝐹:𝑋⟶𝑌 → ran ◡𝐹 = 𝑋) |
16 | 12, 15 | syl5sseq 3653 |
. . . . . . . 8
⊢ (𝐹:𝑋⟶𝑌 → (◡𝐹 “ 𝑦) ⊆ 𝑋) |
17 | 1, 16 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (◡𝐹 “ 𝑦) ⊆ 𝑋) |
18 | | df-ss 3588 |
. . . . . . 7
⊢ ((◡𝐹 “ 𝑦) ⊆ 𝑋 ↔ ((◡𝐹 “ 𝑦) ∩ 𝑋) = (◡𝐹 “ 𝑦)) |
19 | 17, 18 | sylib 208 |
. . . . . 6
⊢ (𝜑 → ((◡𝐹 “ 𝑦) ∩ 𝑋) = (◡𝐹 “ 𝑦)) |
20 | 3, 11, 19 | 3eqtr3rd 2665 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ 𝑦) = ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦))) |
21 | 20 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝑦) = ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦))) |
22 | | paste.4 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (Clsd‘𝐽)) |
23 | 22 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → 𝐴 ∈ (Clsd‘𝐽)) |
24 | | paste.8 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾)) |
25 | | cnclima 21072 |
. . . . . . 7
⊢ (((𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐴))) |
26 | 24, 25 | sylan 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐴))) |
27 | | restcldr 20978 |
. . . . . 6
⊢ ((𝐴 ∈ (Clsd‘𝐽) ∧ (◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐴))) → (◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘𝐽)) |
28 | 23, 26, 27 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘𝐽)) |
29 | | paste.5 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ (Clsd‘𝐽)) |
30 | 29 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → 𝐵 ∈ (Clsd‘𝐽)) |
31 | | paste.9 |
. . . . . . 7
⊢ (𝜑 → (𝐹 ↾ 𝐵) ∈ ((𝐽 ↾t 𝐵) Cn 𝐾)) |
32 | | cnclima 21072 |
. . . . . . 7
⊢ (((𝐹 ↾ 𝐵) ∈ ((𝐽 ↾t 𝐵) Cn 𝐾) ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐵))) |
33 | 31, 32 | sylan 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐵))) |
34 | | restcldr 20978 |
. . . . . 6
⊢ ((𝐵 ∈ (Clsd‘𝐽) ∧ (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘(𝐽 ↾t 𝐵))) → (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘𝐽)) |
35 | 30, 33, 34 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘𝐽)) |
36 | | uncld 20845 |
. . . . 5
⊢ (((◡(𝐹 ↾ 𝐴) “ 𝑦) ∈ (Clsd‘𝐽) ∧ (◡(𝐹 ↾ 𝐵) “ 𝑦) ∈ (Clsd‘𝐽)) → ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦)) ∈ (Clsd‘𝐽)) |
37 | 28, 35, 36 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → ((◡(𝐹 ↾ 𝐴) “ 𝑦) ∪ (◡(𝐹 ↾ 𝐵) “ 𝑦)) ∈ (Clsd‘𝐽)) |
38 | 21, 37 | eqeltrd 2701 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (Clsd‘𝐾)) → (◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)) |
39 | 38 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ (Clsd‘𝐾)(◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)) |
40 | | cldrcl 20830 |
. . . 4
⊢ (𝐴 ∈ (Clsd‘𝐽) → 𝐽 ∈ Top) |
41 | 22, 40 | syl 17 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
42 | | cntop2 21045 |
. . . 4
⊢ ((𝐹 ↾ 𝐴) ∈ ((𝐽 ↾t 𝐴) Cn 𝐾) → 𝐾 ∈ Top) |
43 | 24, 42 | syl 17 |
. . 3
⊢ (𝜑 → 𝐾 ∈ Top) |
44 | | paste.1 |
. . . . 5
⊢ 𝑋 = ∪
𝐽 |
45 | 44 | toptopon 20722 |
. . . 4
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
46 | | paste.2 |
. . . . 5
⊢ 𝑌 = ∪
𝐾 |
47 | 46 | toptopon 20722 |
. . . 4
⊢ (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘𝑌)) |
48 | | iscncl 21073 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)))) |
49 | 45, 47, 48 | syl2anb 496 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)))) |
50 | 41, 43, 49 | syl2anc 693 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ (Clsd‘𝐾)(◡𝐹 “ 𝑦) ∈ (Clsd‘𝐽)))) |
51 | 1, 39, 50 | mpbir2and 957 |
1
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |