Step | Hyp | Ref
| Expression |
1 | | qtopomap.5 |
. . 3
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
2 | | qtopomap.4 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
3 | | qtopomap.6 |
. . 3
⊢ (𝜑 → ran 𝐹 = 𝑌) |
4 | | qtopss 21328 |
. . 3
⊢ ((𝐹 ∈ (𝐽 Cn 𝐾) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ ran 𝐹 = 𝑌) → 𝐾 ⊆ (𝐽 qTop 𝐹)) |
5 | 1, 2, 3, 4 | syl3anc 1318 |
. 2
⊢ (𝜑 → 𝐾 ⊆ (𝐽 qTop 𝐹)) |
6 | | cntop1 20854 |
. . . . . . 7
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐽 ∈ Top) |
7 | 1, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Top) |
8 | | eqid 2610 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
9 | 8 | toptopon 20548 |
. . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
10 | 7, 9 | sylib 207 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
11 | | cnf2 20863 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐾 ∈
(TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:∪ 𝐽⟶𝑌) |
12 | 10, 2, 1, 11 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → 𝐹:∪ 𝐽⟶𝑌) |
13 | | ffn 5958 |
. . . . . . 7
⊢ (𝐹:∪
𝐽⟶𝑌 → 𝐹 Fn ∪ 𝐽) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹 Fn ∪ 𝐽) |
15 | | df-fo 5810 |
. . . . . 6
⊢ (𝐹:∪
𝐽–onto→𝑌 ↔ (𝐹 Fn ∪ 𝐽 ∧ ran 𝐹 = 𝑌)) |
16 | 14, 3, 15 | sylanbrc 695 |
. . . . 5
⊢ (𝜑 → 𝐹:∪ 𝐽–onto→𝑌) |
17 | | elqtop3 21316 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐹:∪ 𝐽–onto→𝑌) → (𝑦 ∈ (𝐽 qTop 𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽))) |
18 | 10, 16, 17 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ (𝐽 qTop 𝐹) ↔ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽))) |
19 | | foimacnv 6067 |
. . . . . . . 8
⊢ ((𝐹:∪
𝐽–onto→𝑌 ∧ 𝑦 ⊆ 𝑌) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
20 | 16, 19 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ⊆ 𝑌) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
21 | 20 | adantrr 749 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝐹 “ (◡𝐹 “ 𝑦)) = 𝑦) |
22 | | simprr 792 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ 𝑦) ∈ 𝐽) |
23 | | qtopomap.7 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐾) |
24 | 23 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ 𝐾) |
25 | 24 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → ∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ 𝐾) |
26 | | imaeq2 5381 |
. . . . . . . . 9
⊢ (𝑥 = (◡𝐹 “ 𝑦) → (𝐹 “ 𝑥) = (𝐹 “ (◡𝐹 “ 𝑦))) |
27 | 26 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = (◡𝐹 “ 𝑦) → ((𝐹 “ 𝑥) ∈ 𝐾 ↔ (𝐹 “ (◡𝐹 “ 𝑦)) ∈ 𝐾)) |
28 | 27 | rspcv 3278 |
. . . . . . 7
⊢ ((◡𝐹 “ 𝑦) ∈ 𝐽 → (∀𝑥 ∈ 𝐽 (𝐹 “ 𝑥) ∈ 𝐾 → (𝐹 “ (◡𝐹 “ 𝑦)) ∈ 𝐾)) |
29 | 22, 25, 28 | sylc 63 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → (𝐹 “ (◡𝐹 “ 𝑦)) ∈ 𝐾) |
30 | 21, 29 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑦 ∈ 𝐾) |
31 | 30 | ex 449 |
. . . 4
⊢ (𝜑 → ((𝑦 ⊆ 𝑌 ∧ (◡𝐹 “ 𝑦) ∈ 𝐽) → 𝑦 ∈ 𝐾)) |
32 | 18, 31 | sylbid 229 |
. . 3
⊢ (𝜑 → (𝑦 ∈ (𝐽 qTop 𝐹) → 𝑦 ∈ 𝐾)) |
33 | 32 | ssrdv 3574 |
. 2
⊢ (𝜑 → (𝐽 qTop 𝐹) ⊆ 𝐾) |
34 | 5, 33 | eqssd 3585 |
1
⊢ (𝜑 → 𝐾 = (𝐽 qTop 𝐹)) |