Step | Hyp | Ref
| Expression |
1 | | qtopomap.5 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
2 | | qtopomap.4 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
3 | | qtopomap.6 |
. . 3
⊢ (𝜑 → ran 𝐹 = 𝑌) |
4 | | qtopss 21518 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 = 𝑌) → 𝐾 ⊆ (𝐽 qTop 𝐹)) |
5 | 1, 2, 3, 4 | syl3anc 1326 |
. 2
⊢ (𝜑 → 𝐾 ⊆ (𝐽 qTop 𝐹)) |
6 | | cntop1 21044 |
. . . . . 6
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
7 | 1, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ Top) |
8 | | eqid 2622 |
. . . . . . . . . 10
⊢ ∪ 𝐽 =
∪ 𝐽 |
9 | 8 | toptopon 20722 |
. . . . . . . . 9
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
10 | 7, 9 | sylib 208 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
11 | | cnf2 21053 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐾 ∈
(TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:∪ 𝐽⟶𝑌) |
12 | 10, 2, 1, 11 | syl3anc 1326 |
. . . . . . 7
⊢ (𝜑 → 𝐹:∪ 𝐽⟶𝑌) |
13 | | ffn 6045 |
. . . . . . 7
⊢ (𝐹:∪
𝐽⟶𝑌 → 𝐹 Fn ∪ 𝐽) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn ∪ 𝐽) |
15 | | df-fo 5894 |
. . . . . 6
⊢ (𝐹:∪
𝐽–onto→𝑌 ↔ (𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 = 𝑌)) |
16 | 14, 3, 15 | sylanbrc 698 |
. . . . 5
⊢ (𝜑 → 𝐹:∪ 𝐽–onto→𝑌) |
17 | 8 | elqtop2 21504 |
. . . . 5
⊢ ((𝐽 ∈ Top ∧ 𝐹:∪
𝐽–onto→𝑌) → (𝑦 ∈ (𝐽 qTop 𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽))) |
18 | 7, 16, 17 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐽 qTop 𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽))) |
19 | 16 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝐹:∪ 𝐽–onto→𝑌) |
20 | | difss 3737 |
. . . . . . . . 9
⊢ (𝑌 ∖ 𝑦) ⊆ 𝑌 |
21 | | foimacnv 6154 |
. . . . . . . . 9
⊢ ((𝐹:∪
𝐽–onto→𝑌 ∧ (𝑌 ∖ 𝑦) ⊆ 𝑌) → (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))) = (𝑌 ∖ 𝑦)) |
22 | 19, 20, 21 | sylancl 694 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))) = (𝑌 ∖ 𝑦)) |
23 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝐾 ∈ (TopOn‘𝑌)) |
24 | | toponuni 20719 |
. . . . . . . . . 10
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝑌 = ∪ 𝐾) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑌 = ∪ 𝐾) |
26 | 25 | difeq1d 3727 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝑌 ∖ 𝑦) = (∪ 𝐾 ∖ 𝑦)) |
27 | 22, 26 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))) = (∪ 𝐾 ∖ 𝑦)) |
28 | | fofun 6116 |
. . . . . . . . . . 11
⊢ (𝐹:∪
𝐽–onto→𝑌 → Fun 𝐹) |
29 | | funcnvcnv 5956 |
. . . . . . . . . . 11
⊢ (Fun
𝐹 → Fun ◡◡𝐹) |
30 | | imadif 5973 |
. . . . . . . . . . 11
⊢ (Fun
◡◡𝐹 → (◡𝐹 “ (𝑌 ∖ 𝑦)) = ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝑦))) |
31 | 19, 28, 29, 30 | 4syl 19 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ (𝑌 ∖ 𝑦)) = ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝑦))) |
32 | 12 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝐹:∪ 𝐽⟶𝑌) |
33 | | fimacnv 6347 |
. . . . . . . . . . . 12
⊢ (𝐹:∪
𝐽⟶𝑌 → (◡𝐹 “ 𝑌) = ∪ 𝐽) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ 𝑌) = ∪ 𝐽) |
35 | 34 | difeq1d 3727 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → ((◡𝐹 “ 𝑌) ∖ (◡𝐹 “ 𝑦)) = (∪ 𝐽 ∖ (◡𝐹 “ 𝑦))) |
36 | 31, 35 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ (𝑌 ∖ 𝑦)) = (∪ 𝐽 ∖ (◡𝐹 “ 𝑦))) |
37 | 7 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝐽 ∈ Top) |
38 | | simprr 796 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ 𝑦) ∈ 𝐽) |
39 | 8 | opncld 20837 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ (◡𝐹 “ 𝑦) ∈ 𝐽) → (∪ 𝐽 ∖ (◡𝐹 “ 𝑦)) ∈ (Clsd‘𝐽)) |
40 | 37, 38, 39 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (∪
𝐽 ∖ (◡𝐹 “ 𝑦)) ∈ (Clsd‘𝐽)) |
41 | 36, 40 | eqeltrd 2701 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ (𝑌 ∖ 𝑦)) ∈ (Clsd‘𝐽)) |
42 | | qtopcmap.7 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → (𝐹 “ 𝑥) ∈ (Clsd‘𝐾)) |
43 | 42 | ralrimiva 2966 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ (Clsd‘𝐽)(𝐹 “ 𝑥) ∈ (Clsd‘𝐾)) |
44 | 43 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → ∀𝑥 ∈ (Clsd‘𝐽)(𝐹 “ 𝑥) ∈ (Clsd‘𝐾)) |
45 | | imaeq2 5462 |
. . . . . . . . . 10
⊢ (𝑥 = (◡𝐹 “ (𝑌 ∖ 𝑦)) → (𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦)))) |
46 | 45 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑥 = (◡𝐹 “ (𝑌 ∖ 𝑦)) → ((𝐹 “ 𝑥) ∈ (Clsd‘𝐾) ↔ (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))) ∈ (Clsd‘𝐾))) |
47 | 46 | rspcv 3305 |
. . . . . . . 8
⊢ ((◡𝐹 “ (𝑌 ∖ 𝑦)) ∈ (Clsd‘𝐽) → (∀𝑥 ∈ (Clsd‘𝐽)(𝐹 “ 𝑥) ∈ (Clsd‘𝐾) → (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))) ∈ (Clsd‘𝐾))) |
48 | 41, 44, 47 | sylc 65 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝐹 “ (◡𝐹 “ (𝑌 ∖ 𝑦))) ∈ (Clsd‘𝐾)) |
49 | 27, 48 | eqeltrrd 2702 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (∪
𝐾 ∖ 𝑦) ∈ (Clsd‘𝐾)) |
50 | | topontop 20718 |
. . . . . . . 8
⊢ (𝐾 ∈ (TopOn‘𝑌) → 𝐾 ∈ Top) |
51 | 23, 50 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝐾 ∈ Top) |
52 | | simprl 794 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑦 ⊆ 𝑌) |
53 | 52, 25 | sseqtrd 3641 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑦 ⊆ ∪ 𝐾) |
54 | | eqid 2622 |
. . . . . . . 8
⊢ ∪ 𝐾 =
∪ 𝐾 |
55 | 54 | isopn2 20836 |
. . . . . . 7
⊢ ((𝐾 ∈ Top ∧ 𝑦 ⊆ ∪ 𝐾)
→ (𝑦 ∈ 𝐾 ↔ (∪ 𝐾
∖ 𝑦) ∈
(Clsd‘𝐾))) |
56 | 51, 53, 55 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝑦 ∈ 𝐾 ↔ (∪ 𝐾 ∖ 𝑦) ∈ (Clsd‘𝐾))) |
57 | 49, 56 | mpbird 247 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑦 ∈ 𝐾) |
58 | 57 | ex 450 |
. . . 4
⊢ (𝜑 → ((𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽) → 𝑦 ∈ 𝐾)) |
59 | 18, 58 | sylbid 230 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐽 qTop 𝐹) → 𝑦 ∈ 𝐾)) |
60 | 59 | ssrdv 3609 |
. 2
⊢ (𝜑 → (𝐽 qTop 𝐹) ⊆ 𝐾) |
61 | 5, 60 | eqssd 3620 |
1
⊢ (𝜑 → 𝐾 = (𝐽 qTop 𝐹)) |