Step | Hyp | Ref
| Expression |
1 | | qtophmeo.2 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | qtophmeo.3 |
. . . . 5
⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) |
3 | | qtophmeo.4 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝑋–onto→𝑌) |
4 | | fofn 6117 |
. . . . . . 7
⊢ (𝐺:𝑋–onto→𝑌 → 𝐺 Fn 𝑋) |
5 | 3, 4 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 Fn 𝑋) |
6 | | qtopid 21508 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐺 Fn 𝑋) → 𝐺 ∈ (𝐽 Cn (𝐽 qTop 𝐺))) |
7 | 1, 5, 6 | syl2anc 693 |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝐽 Cn (𝐽 qTop 𝐺))) |
8 | | df-3an 1039 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦)) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) |
9 | | qtophmeo.5 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥) = (𝐹‘𝑦) ↔ (𝐺‘𝑥) = (𝐺‘𝑦))) |
10 | 9 | biimpd 219 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐹‘𝑥) = (𝐹‘𝑦) → (𝐺‘𝑥) = (𝐺‘𝑦))) |
11 | 10 | impr 649 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐺‘𝑥) = (𝐺‘𝑦)) |
12 | 8, 11 | sylan2b 492 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐺‘𝑥) = (𝐺‘𝑦)) |
13 | 1, 2, 7, 12 | qtopeu 21519 |
. . . 4
⊢ (𝜑 → ∃!𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺))𝐺 = (𝑓 ∘ 𝐹)) |
14 | | reurex 3160 |
. . . 4
⊢
(∃!𝑓 ∈
((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺))𝐺 = (𝑓 ∘ 𝐹) → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺))𝐺 = (𝑓 ∘ 𝐹)) |
15 | 13, 14 | syl 17 |
. . 3
⊢ (𝜑 → ∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺))𝐺 = (𝑓 ∘ 𝐹)) |
16 | | simprl 794 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) → 𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺))) |
17 | | fofn 6117 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹 Fn 𝑋) |
18 | 2, 17 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 Fn 𝑋) |
19 | | qtopid 21508 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 Fn 𝑋) → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) |
20 | 1, 18, 19 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹))) |
21 | | df-3an 1039 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐺‘𝑥) = (𝐺‘𝑦)) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐺‘𝑥) = (𝐺‘𝑦))) |
22 | 9 | biimprd 238 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → ((𝐺‘𝑥) = (𝐺‘𝑦) → (𝐹‘𝑥) = (𝐹‘𝑦))) |
23 | 22 | impr 649 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (𝐺‘𝑥) = (𝐺‘𝑦))) → (𝐹‘𝑥) = (𝐹‘𝑦)) |
24 | 21, 23 | sylan2b 492 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐺‘𝑥) = (𝐺‘𝑦))) → (𝐹‘𝑥) = (𝐹‘𝑦)) |
25 | 1, 3, 20, 24 | qtopeu 21519 |
. . . . . . . . . 10
⊢ (𝜑 → ∃!𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹))𝐹 = (𝑔 ∘ 𝐺)) |
26 | 25 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) → ∃!𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹))𝐹 = (𝑔 ∘ 𝐺)) |
27 | | reurex 3160 |
. . . . . . . . 9
⊢
(∃!𝑔 ∈
((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹))𝐹 = (𝑔 ∘ 𝐺) → ∃𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹))𝐹 = (𝑔 ∘ 𝐺)) |
28 | 26, 27 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) → ∃𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹))𝐹 = (𝑔 ∘ 𝐺)) |
29 | | qtoptopon 21507 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹:𝑋–onto→𝑌) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
30 | 1, 2, 29 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
31 | 30 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
32 | | qtoptopon 21507 |
. . . . . . . . . . . . 13
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐺:𝑋–onto→𝑌) → (𝐽 qTop 𝐺) ∈ (TopOn‘𝑌)) |
33 | 1, 3, 32 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐽 qTop 𝐺) ∈ (TopOn‘𝑌)) |
34 | 33 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → (𝐽 qTop 𝐺) ∈ (TopOn‘𝑌)) |
35 | | simplrl 800 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺))) |
36 | | cnf2 21053 |
. . . . . . . . . . 11
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ (𝐽 qTop 𝐺) ∈ (TopOn‘𝑌) ∧ 𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺))) → 𝑓:𝑌⟶𝑌) |
37 | 31, 34, 35, 36 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝑓:𝑌⟶𝑌) |
38 | | simprl 794 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹))) |
39 | | cnf2 21053 |
. . . . . . . . . . 11
⊢ (((𝐽 qTop 𝐺) ∈ (TopOn‘𝑌) ∧ (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ 𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹))) → 𝑔:𝑌⟶𝑌) |
40 | 34, 31, 38, 39 | syl3anc 1326 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝑔:𝑌⟶𝑌) |
41 | | coeq1 5279 |
. . . . . . . . . . . 12
⊢ (ℎ = (𝑔 ∘ 𝑓) → (ℎ ∘ 𝐹) = ((𝑔 ∘ 𝑓) ∘ 𝐹)) |
42 | 41 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (ℎ = (𝑔 ∘ 𝑓) → (𝐹 = (ℎ ∘ 𝐹) ↔ 𝐹 = ((𝑔 ∘ 𝑓) ∘ 𝐹))) |
43 | | coeq1 5279 |
. . . . . . . . . . . 12
⊢ (ℎ = ( I ↾ 𝑌) → (ℎ ∘ 𝐹) = (( I ↾ 𝑌) ∘ 𝐹)) |
44 | 43 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (ℎ = ( I ↾ 𝑌) → (𝐹 = (ℎ ∘ 𝐹) ↔ 𝐹 = (( I ↾ 𝑌) ∘ 𝐹))) |
45 | | simpr3 1069 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐹‘𝑥) = (𝐹‘𝑦))) → (𝐹‘𝑥) = (𝐹‘𝑦)) |
46 | 1, 2, 20, 45 | qtopeu 21519 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∃!ℎ ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐹))𝐹 = (ℎ ∘ 𝐹)) |
47 | 46 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → ∃!ℎ ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐹))𝐹 = (ℎ ∘ 𝐹)) |
48 | | cnco 21070 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹))) → (𝑔 ∘ 𝑓) ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐹))) |
49 | 35, 38, 48 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → (𝑔 ∘ 𝑓) ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐹))) |
50 | | idcn 21061 |
. . . . . . . . . . . . 13
⊢ ((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) → ( I ↾ 𝑌) ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐹))) |
51 | 30, 50 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ( I ↾ 𝑌) ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐹))) |
52 | 51 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → ( I ↾ 𝑌) ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐹))) |
53 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝐹 = (𝑔 ∘ 𝐺)) |
54 | | simplrr 801 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝐺 = (𝑓 ∘ 𝐹)) |
55 | 54 | coeq2d 5284 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → (𝑔 ∘ 𝐺) = (𝑔 ∘ (𝑓 ∘ 𝐹))) |
56 | 53, 55 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝐹 = (𝑔 ∘ (𝑓 ∘ 𝐹))) |
57 | | coass 5654 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∘ 𝑓) ∘ 𝐹) = (𝑔 ∘ (𝑓 ∘ 𝐹)) |
58 | 56, 57 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝐹 = ((𝑔 ∘ 𝑓) ∘ 𝐹)) |
59 | | fof 6115 |
. . . . . . . . . . . . . . 15
⊢ (𝐹:𝑋–onto→𝑌 → 𝐹:𝑋⟶𝑌) |
60 | 2, 59 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) |
61 | 60 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝐹:𝑋⟶𝑌) |
62 | | fcoi2 6079 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝑋⟶𝑌 → (( I ↾ 𝑌) ∘ 𝐹) = 𝐹) |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → (( I ↾ 𝑌) ∘ 𝐹) = 𝐹) |
64 | 63 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝐹 = (( I ↾ 𝑌) ∘ 𝐹)) |
65 | 42, 44, 47, 49, 52, 58, 64 | reu2eqd 3403 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → (𝑔 ∘ 𝑓) = ( I ↾ 𝑌)) |
66 | | coeq1 5279 |
. . . . . . . . . . . 12
⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ ∘ 𝐺) = ((𝑓 ∘ 𝑔) ∘ 𝐺)) |
67 | 66 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (ℎ = (𝑓 ∘ 𝑔) → (𝐺 = (ℎ ∘ 𝐺) ↔ 𝐺 = ((𝑓 ∘ 𝑔) ∘ 𝐺))) |
68 | | coeq1 5279 |
. . . . . . . . . . . 12
⊢ (ℎ = ( I ↾ 𝑌) → (ℎ ∘ 𝐺) = (( I ↾ 𝑌) ∘ 𝐺)) |
69 | 68 | eqeq2d 2632 |
. . . . . . . . . . 11
⊢ (ℎ = ( I ↾ 𝑌) → (𝐺 = (ℎ ∘ 𝐺) ↔ 𝐺 = (( I ↾ 𝑌) ∘ 𝐺))) |
70 | | simpr3 1069 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ (𝐺‘𝑥) = (𝐺‘𝑦))) → (𝐺‘𝑥) = (𝐺‘𝑦)) |
71 | 1, 3, 7, 70 | qtopeu 21519 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∃!ℎ ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐺))𝐺 = (ℎ ∘ 𝐺)) |
72 | 71 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → ∃!ℎ ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐺))𝐺 = (ℎ ∘ 𝐺)) |
73 | | cnco 21070 |
. . . . . . . . . . . 12
⊢ ((𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺))) → (𝑓 ∘ 𝑔) ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐺))) |
74 | 38, 35, 73 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → (𝑓 ∘ 𝑔) ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐺))) |
75 | | idcn 21061 |
. . . . . . . . . . . . 13
⊢ ((𝐽 qTop 𝐺) ∈ (TopOn‘𝑌) → ( I ↾ 𝑌) ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐺))) |
76 | 33, 75 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ( I ↾ 𝑌) ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐺))) |
77 | 76 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → ( I ↾ 𝑌) ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐺))) |
78 | 53 | coeq2d 5284 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → (𝑓 ∘ 𝐹) = (𝑓 ∘ (𝑔 ∘ 𝐺))) |
79 | 54, 78 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝐺 = (𝑓 ∘ (𝑔 ∘ 𝐺))) |
80 | | coass 5654 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∘ 𝑔) ∘ 𝐺) = (𝑓 ∘ (𝑔 ∘ 𝐺)) |
81 | 79, 80 | syl6eqr 2674 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝐺 = ((𝑓 ∘ 𝑔) ∘ 𝐺)) |
82 | | fof 6115 |
. . . . . . . . . . . . . . 15
⊢ (𝐺:𝑋–onto→𝑌 → 𝐺:𝑋⟶𝑌) |
83 | 3, 82 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:𝑋⟶𝑌) |
84 | 83 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝐺:𝑋⟶𝑌) |
85 | | fcoi2 6079 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝑋⟶𝑌 → (( I ↾ 𝑌) ∘ 𝐺) = 𝐺) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → (( I ↾ 𝑌) ∘ 𝐺) = 𝐺) |
87 | 86 | eqcomd 2628 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → 𝐺 = (( I ↾ 𝑌) ∘ 𝐺)) |
88 | 67, 69, 72, 74, 77, 81, 87 | reu2eqd 3403 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → (𝑓 ∘ 𝑔) = ( I ↾ 𝑌)) |
89 | 37, 40, 65, 88 | 2fcoidinvd 6550 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → ◡𝑓 = 𝑔) |
90 | 89, 38 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) ∧ (𝑔 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)) ∧ 𝐹 = (𝑔 ∘ 𝐺))) → ◡𝑓 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹))) |
91 | 28, 90 | rexlimddv 3035 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) → ◡𝑓 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹))) |
92 | | ishmeo 21562 |
. . . . . . 7
⊢ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ↔ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ ◡𝑓 ∈ ((𝐽 qTop 𝐺) Cn (𝐽 qTop 𝐹)))) |
93 | 16, 91, 92 | sylanbrc 698 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) → 𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))) |
94 | | simprr 796 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) → 𝐺 = (𝑓 ∘ 𝐹)) |
95 | 93, 94 | jca 554 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) → (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹))) |
96 | 95 | ex 450 |
. . . 4
⊢ (𝜑 → ((𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹)) → (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝐺 = (𝑓 ∘ 𝐹)))) |
97 | 96 | reximdv2 3014 |
. . 3
⊢ (𝜑 → (∃𝑓 ∈ ((𝐽 qTop 𝐹) Cn (𝐽 qTop 𝐺))𝐺 = (𝑓 ∘ 𝐹) → ∃𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))𝐺 = (𝑓 ∘ 𝐹))) |
98 | 15, 97 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))𝐺 = (𝑓 ∘ 𝐹)) |
99 | | eqtr2 2642 |
. . . 4
⊢ ((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → (𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹)) |
100 | 2 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)))) → 𝐹:𝑋–onto→𝑌) |
101 | 30 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)))) → (𝐽 qTop 𝐹) ∈ (TopOn‘𝑌)) |
102 | 33 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)))) → (𝐽 qTop 𝐺) ∈ (TopOn‘𝑌)) |
103 | | simprl 794 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)))) → 𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))) |
104 | | hmeof1o2 21566 |
. . . . . . 7
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ (𝐽 qTop 𝐺) ∈ (TopOn‘𝑌) ∧ 𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))) → 𝑓:𝑌–1-1-onto→𝑌) |
105 | 101, 102,
103, 104 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)))) → 𝑓:𝑌–1-1-onto→𝑌) |
106 | | f1ofn 6138 |
. . . . . 6
⊢ (𝑓:𝑌–1-1-onto→𝑌 → 𝑓 Fn 𝑌) |
107 | 105, 106 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)))) → 𝑓 Fn 𝑌) |
108 | | simprr 796 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)))) → 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))) |
109 | | hmeof1o2 21566 |
. . . . . . 7
⊢ (((𝐽 qTop 𝐹) ∈ (TopOn‘𝑌) ∧ (𝐽 qTop 𝐺) ∈ (TopOn‘𝑌) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))) → 𝑔:𝑌–1-1-onto→𝑌) |
110 | 101, 102,
108, 109 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)))) → 𝑔:𝑌–1-1-onto→𝑌) |
111 | | f1ofn 6138 |
. . . . . 6
⊢ (𝑔:𝑌–1-1-onto→𝑌 → 𝑔 Fn 𝑌) |
112 | 110, 111 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)))) → 𝑔 Fn 𝑌) |
113 | | cocan2 6547 |
. . . . 5
⊢ ((𝐹:𝑋–onto→𝑌 ∧ 𝑓 Fn 𝑌 ∧ 𝑔 Fn 𝑌) → ((𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹) ↔ 𝑓 = 𝑔)) |
114 | 100, 107,
112, 113 | syl3anc 1326 |
. . . 4
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)))) → ((𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹) ↔ 𝑓 = 𝑔)) |
115 | 99, 114 | syl5ib 234 |
. . 3
⊢ ((𝜑 ∧ (𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)) ∧ 𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺)))) → ((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔)) |
116 | 115 | ralrimivva 2971 |
. 2
⊢ (𝜑 → ∀𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))∀𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔)) |
117 | | coeq1 5279 |
. . . 4
⊢ (𝑓 = 𝑔 → (𝑓 ∘ 𝐹) = (𝑔 ∘ 𝐹)) |
118 | 117 | eqeq2d 2632 |
. . 3
⊢ (𝑓 = 𝑔 → (𝐺 = (𝑓 ∘ 𝐹) ↔ 𝐺 = (𝑔 ∘ 𝐹))) |
119 | 118 | reu4 3400 |
. 2
⊢
(∃!𝑓 ∈
((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))𝐺 = (𝑓 ∘ 𝐹) ↔ (∃𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))𝐺 = (𝑓 ∘ 𝐹) ∧ ∀𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))∀𝑔 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))((𝐺 = (𝑓 ∘ 𝐹) ∧ 𝐺 = (𝑔 ∘ 𝐹)) → 𝑓 = 𝑔))) |
120 | 98, 116, 119 | sylanbrc 698 |
1
⊢ (𝜑 → ∃!𝑓 ∈ ((𝐽 qTop 𝐹)Homeo(𝐽 qTop 𝐺))𝐺 = (𝑓 ∘ 𝐹)) |