Metamath Proof Explorer

Theorem qtophmeo

Description: If two functions on a base topology J make the same identifications in order to create quotient spaces J qTop F and J qTop G , then not only are J qTop F and J qTop G homeomorphic, but there is a unique homeomorphism that makes the diagram commute. (Contributed by Mario Carneiro, 24-Mar-2015) (Proof shortened by Mario Carneiro, 23-Aug-2015)

Ref Expression
Hypotheses qtophmeo.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
qtophmeo.3 ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
qtophmeo.4 ⊢ ( 𝜑 → 𝐺 : 𝑋 –onto→ 𝑌 )
qtophmeo.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) )
Assertion qtophmeo ( 𝜑 → ∃! 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) 𝐺 = ( 𝑓 ∘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 qtophmeo.2 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 qtophmeo.3 ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
3 qtophmeo.4 ⊢ ( 𝜑 → 𝐺 : 𝑋 –onto→ 𝑌 )
4 qtophmeo.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) )
5 fofn ⊢ ( 𝐺 : 𝑋 –onto→ 𝑌 → 𝐺 Fn 𝑋 )
6 3 5 syl ⊢ ( 𝜑 → 𝐺 Fn 𝑋 )
7 qtopid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐺 Fn 𝑋 ) → 𝐺 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐺 ) ) )
8 1 6 7 syl2anc ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐺 ) ) )
9 df-3an ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
10 4 biimpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) )
11 10 impr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) )
12 9 11 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) )
13 1 2 8 12 qtopeu ⊢ ( 𝜑 → ∃! 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) 𝐺 = ( 𝑓 ∘ 𝐹 ) )
14 reurex ⊢ ( ∃! 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) 𝐺 = ( 𝑓 ∘ 𝐹 ) → ∃ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) 𝐺 = ( 𝑓 ∘ 𝐹 ) )
15 13 14 syl ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) 𝐺 = ( 𝑓 ∘ 𝐹 ) )
16 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) → 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) )
17 fofn ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 Fn 𝑋 )
18 2 17 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
19 qtopid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 Fn 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
20 1 18 19 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn ( 𝐽 qTop 𝐹 ) ) )
21 df-3an ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) )
22 4 biimprd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
23 22 impr ⊢ ( ( 𝜑 ∧ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
24 21 23 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
25 1 3 20 24 qtopeu ⊢ ( 𝜑 → ∃! 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) 𝐹 = ( 𝑔 ∘ 𝐺 ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) → ∃! 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) 𝐹 = ( 𝑔 ∘ 𝐺 ) )
27 reurex ⊢ ( ∃! 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) 𝐹 = ( 𝑔 ∘ 𝐺 ) → ∃ 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) 𝐹 = ( 𝑔 ∘ 𝐺 ) )
28 26 27 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) → ∃ 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) 𝐹 = ( 𝑔 ∘ 𝐺 ) )
29 qtoptopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
30 1 2 29 syl2anc ⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
31 30 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
32 qtoptopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐺 : 𝑋 –onto→ 𝑌 ) → ( 𝐽 qTop 𝐺 ) ∈ ( TopOn ‘ 𝑌 ) )
33 1 3 32 syl2anc ⊢ ( 𝜑 → ( 𝐽 qTop 𝐺 ) ∈ ( TopOn ‘ 𝑌 ) )
34 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( 𝐽 qTop 𝐺 ) ∈ ( TopOn ‘ 𝑌 ) )
35 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) )
36 cnf2 ⊢ ( ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) ∧ ( 𝐽 qTop 𝐺 ) ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ) → 𝑓 : 𝑌 ⟶ 𝑌 )
37 31 34 35 36 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝑓 : 𝑌 ⟶ 𝑌 )
38 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) )
39 cnf2 ⊢ ( ( ( 𝐽 qTop 𝐺 ) ∈ ( TopOn ‘ 𝑌 ) ∧ ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ) → 𝑔 : 𝑌 ⟶ 𝑌 )
40 34 31 38 39 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝑔 : 𝑌 ⟶ 𝑌 )
41 coeq1 ⊢ ( ℎ = ( 𝑔 ∘ 𝑓 ) → ( ℎ ∘ 𝐹 ) = ( ( 𝑔 ∘ 𝑓 ) ∘ 𝐹 ) )
42 41 eqeq2d ⊢ ( ℎ = ( 𝑔 ∘ 𝑓 ) → ( 𝐹 = ( ℎ ∘ 𝐹 ) ↔ 𝐹 = ( ( 𝑔 ∘ 𝑓 ) ∘ 𝐹 ) ) )
43 coeq1 ⊢ ( ℎ = ( I ↾ 𝑌 ) → ( ℎ ∘ 𝐹 ) = ( ( I ↾ 𝑌 ) ∘ 𝐹 ) )
44 43 eqeq2d ⊢ ( ℎ = ( I ↾ 𝑌 ) → ( 𝐹 = ( ℎ ∘ 𝐹 ) ↔ 𝐹 = ( ( I ↾ 𝑌 ) ∘ 𝐹 ) ) )
45 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
46 1 2 20 45 qtopeu ⊢ ( 𝜑 → ∃! ℎ ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐹 ) ) 𝐹 = ( ℎ ∘ 𝐹 ) )
47 46 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ∃! ℎ ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐹 ) ) 𝐹 = ( ℎ ∘ 𝐹 ) )
48 cnco ⊢ ( ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐹 ) ) )
49 35 38 48 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( 𝑔 ∘ 𝑓 ) ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐹 ) ) )
50 idcn ⊢ ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) → ( I ↾ 𝑌 ) ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐹 ) ) )
51 30 50 syl ⊢ ( 𝜑 → ( I ↾ 𝑌 ) ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐹 ) ) )
52 51 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( I ↾ 𝑌 ) ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐹 ) ) )
53 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝐹 = ( 𝑔 ∘ 𝐺 ) )
54 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝐺 = ( 𝑓 ∘ 𝐹 ) )
55 54 coeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( 𝑔 ∘ 𝐺 ) = ( 𝑔 ∘ ( 𝑓 ∘ 𝐹 ) ) )
56 53 55 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝐹 = ( 𝑔 ∘ ( 𝑓 ∘ 𝐹 ) ) )
57 coass ⊢ ( ( 𝑔 ∘ 𝑓 ) ∘ 𝐹 ) = ( 𝑔 ∘ ( 𝑓 ∘ 𝐹 ) )
58 56 57 eqtr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝐹 = ( ( 𝑔 ∘ 𝑓 ) ∘ 𝐹 ) )
59 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
60 2 59 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
61 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝐹 : 𝑋 ⟶ 𝑌 )
62 fcoi2 ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → ( ( I ↾ 𝑌 ) ∘ 𝐹 ) = 𝐹 )
63 61 62 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( ( I ↾ 𝑌 ) ∘ 𝐹 ) = 𝐹 )
64 63 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝐹 = ( ( I ↾ 𝑌 ) ∘ 𝐹 ) )
65 42 44 47 49 52 58 64 reu2eqd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( 𝑔 ∘ 𝑓 ) = ( I ↾ 𝑌 ) )
66 coeq1 ⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( ℎ ∘ 𝐺 ) = ( ( 𝑓 ∘ 𝑔 ) ∘ 𝐺 ) )
67 66 eqeq2d ⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( 𝐺 = ( ℎ ∘ 𝐺 ) ↔ 𝐺 = ( ( 𝑓 ∘ 𝑔 ) ∘ 𝐺 ) ) )
68 coeq1 ⊢ ( ℎ = ( I ↾ 𝑌 ) → ( ℎ ∘ 𝐺 ) = ( ( I ↾ 𝑌 ) ∘ 𝐺 ) )
69 68 eqeq2d ⊢ ( ℎ = ( I ↾ 𝑌 ) → ( 𝐺 = ( ℎ ∘ 𝐺 ) ↔ 𝐺 = ( ( I ↾ 𝑌 ) ∘ 𝐺 ) ) )
70 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) )
71 1 3 8 70 qtopeu ⊢ ( 𝜑 → ∃! ℎ ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐺 ) ) 𝐺 = ( ℎ ∘ 𝐺 ) )
72 71 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ∃! ℎ ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐺 ) ) 𝐺 = ( ℎ ∘ 𝐺 ) )
73 cnco ⊢ ( ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ) → ( 𝑓 ∘ 𝑔 ) ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐺 ) ) )
74 38 35 73 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( 𝑓 ∘ 𝑔 ) ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐺 ) ) )
75 idcn ⊢ ( ( 𝐽 qTop 𝐺 ) ∈ ( TopOn ‘ 𝑌 ) → ( I ↾ 𝑌 ) ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐺 ) ) )
76 33 75 syl ⊢ ( 𝜑 → ( I ↾ 𝑌 ) ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐺 ) ) )
77 76 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( I ↾ 𝑌 ) ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐺 ) ) )
78 53 coeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( 𝑓 ∘ 𝐹 ) = ( 𝑓 ∘ ( 𝑔 ∘ 𝐺 ) ) )
79 54 78 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝐺 = ( 𝑓 ∘ ( 𝑔 ∘ 𝐺 ) ) )
80 coass ⊢ ( ( 𝑓 ∘ 𝑔 ) ∘ 𝐺 ) = ( 𝑓 ∘ ( 𝑔 ∘ 𝐺 ) )
81 79 80 eqtr4di ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝐺 = ( ( 𝑓 ∘ 𝑔 ) ∘ 𝐺 ) )
82 fof ⊢ ( 𝐺 : 𝑋 –onto→ 𝑌 → 𝐺 : 𝑋 ⟶ 𝑌 )
83 3 82 syl ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ 𝑌 )
84 83 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝐺 : 𝑋 ⟶ 𝑌 )
85 fcoi2 ⊢ ( 𝐺 : 𝑋 ⟶ 𝑌 → ( ( I ↾ 𝑌 ) ∘ 𝐺 ) = 𝐺 )
86 84 85 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( ( I ↾ 𝑌 ) ∘ 𝐺 ) = 𝐺 )
87 86 eqcomd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → 𝐺 = ( ( I ↾ 𝑌 ) ∘ 𝐺 ) )
88 67 69 72 74 77 81 87 reu2eqd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ( 𝑓 ∘ 𝑔 ) = ( I ↾ 𝑌 ) )
89 37 40 65 88 2fcoidinvd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ◡ 𝑓 = 𝑔 )
90 89 38 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) ∧ ( 𝑔 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ∧ 𝐹 = ( 𝑔 ∘ 𝐺 ) ) ) → ◡ 𝑓 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) )
91 28 90 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) → ◡ 𝑓 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) )
92 ishmeo ⊢ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ↔ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ ◡ 𝑓 ∈ ( ( 𝐽 qTop 𝐺 ) Cn ( 𝐽 qTop 𝐹 ) ) ) )
93 16 91 92 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) → 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) )
94 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn ( 𝐽 qTop 𝐺 ) ) ∧ 𝐺 = ( 𝑓 ∘ 𝐹 ) ) ) → 𝐺 = ( 𝑓 ∘ 𝐹 ) )
95 15 93 94 reximssdv ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) 𝐺 = ( 𝑓 ∘ 𝐹 ) )
96 eqtr2 ⊢ ( ( 𝐺 = ( 𝑓 ∘ 𝐹 ) ∧ 𝐺 = ( 𝑔 ∘ 𝐹 ) ) → ( 𝑓 ∘ 𝐹 ) = ( 𝑔 ∘ 𝐹 ) )
97 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) ) → 𝐹 : 𝑋 –onto→ 𝑌 )
98 30 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
99 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) ) → ( 𝐽 qTop 𝐺 ) ∈ ( TopOn ‘ 𝑌 ) )
100 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) ) → 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) )
101 hmeof1o2 ⊢ ( ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) ∧ ( 𝐽 qTop 𝐺 ) ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) → 𝑓 : 𝑌 –1-1-onto→ 𝑌 )
102 98 99 100 101 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) ) → 𝑓 : 𝑌 –1-1-onto→ 𝑌 )
103 f1ofn ⊢ ( 𝑓 : 𝑌 –1-1-onto→ 𝑌 → 𝑓 Fn 𝑌 )
104 102 103 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) ) → 𝑓 Fn 𝑌 )
105 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) ) → 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) )
106 hmeof1o2 ⊢ ( ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) ∧ ( 𝐽 qTop 𝐺 ) ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) → 𝑔 : 𝑌 –1-1-onto→ 𝑌 )
107 98 99 105 106 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) ) → 𝑔 : 𝑌 –1-1-onto→ 𝑌 )
108 f1ofn ⊢ ( 𝑔 : 𝑌 –1-1-onto→ 𝑌 → 𝑔 Fn 𝑌 )
109 107 108 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) ) → 𝑔 Fn 𝑌 )
110 cocan2 ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑓 Fn 𝑌 ∧ 𝑔 Fn 𝑌 ) → ( ( 𝑓 ∘ 𝐹 ) = ( 𝑔 ∘ 𝐹 ) ↔ 𝑓 = 𝑔 ) )
111 97 104 109 110 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) ) → ( ( 𝑓 ∘ 𝐹 ) = ( 𝑔 ∘ 𝐹 ) ↔ 𝑓 = 𝑔 ) )
112 96 111 syl5ib ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ) ) → ( ( 𝐺 = ( 𝑓 ∘ 𝐹 ) ∧ 𝐺 = ( 𝑔 ∘ 𝐹 ) ) → 𝑓 = 𝑔 ) )
113 112 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∀ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ( ( 𝐺 = ( 𝑓 ∘ 𝐹 ) ∧ 𝐺 = ( 𝑔 ∘ 𝐹 ) ) → 𝑓 = 𝑔 ) )
114 coeq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∘ 𝐹 ) = ( 𝑔 ∘ 𝐹 ) )
115 114 eqeq2d ⊢ ( 𝑓 = 𝑔 → ( 𝐺 = ( 𝑓 ∘ 𝐹 ) ↔ 𝐺 = ( 𝑔 ∘ 𝐹 ) ) )
116 115 reu4 ⊢ ( ∃! 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) 𝐺 = ( 𝑓 ∘ 𝐹 ) ↔ ( ∃ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) 𝐺 = ( 𝑓 ∘ 𝐹 ) ∧ ∀ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ∀ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) ( ( 𝐺 = ( 𝑓 ∘ 𝐹 ) ∧ 𝐺 = ( 𝑔 ∘ 𝐹 ) ) → 𝑓 = 𝑔 ) ) )
117 95 113 116 sylanbrc ⊢ ( 𝜑 → ∃! 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Homeo ( 𝐽 qTop 𝐺 ) ) 𝐺 = ( 𝑓 ∘ 𝐹 ) )