Metamath Proof Explorer

Theorem qtopeu

Description: Universal property of the quotient topology. If G is a function from J to K which is equal on all equivalent elements under F , then there is a unique continuous map f : ( J / F ) --> K such that G = f o. F , and we say that G "passes to the quotient". (Contributed by Mario Carneiro, 24-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 qtopeu.1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 qtopeu.3 ⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
3 qtopeu.4 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
4 qtopeu.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) )
5 fofn ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 Fn 𝑋 )
6 2 5 syl ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
7 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 Fn 𝑋 )
8 fniniseg ⊢ ( 𝐹 Fn 𝑋 → ( 𝑦 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
9 7 8 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
10 eqcom ⊢ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
11 10 3anbi3i ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
12 3anass ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
13 11 12 bitri ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
14 13 4 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑦 ) )
15 14 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) ) ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑥 ) )
16 15 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑦 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑥 ) ) )
17 9 16 sylbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑥 ) ) )
18 17 ralrimiv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑥 ) )
19 cntop2 ⊢ ( 𝐺 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
20 3 19 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
21 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
22 20 21 sylib ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
23 cnf2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝐺 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐺 : 𝑋 ⟶ ∪ 𝐾 )
24 1 22 3 23 syl3anc ⊢ ( 𝜑 → 𝐺 : 𝑋 ⟶ ∪ 𝐾 )
25 24 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝑋 )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐺 Fn 𝑋 )
27 cnvimass ⊢ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ dom 𝐹
28 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
29 2 28 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
30 29 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑋 )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → dom 𝐹 = 𝑋 )
32 27 31 sseqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑋 )
33 eqeq1 ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑦 ) → ( 𝑤 = ( 𝐺 ‘ 𝑥 ) ↔ ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑥 ) ) )
34 33 ralima ⊢ ( ( 𝐺 Fn 𝑋 ∧ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ⊆ 𝑋 ) → ( ∀ 𝑤 ∈ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) 𝑤 = ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑥 ) ) )
35 26 32 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∀ 𝑤 ∈ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) 𝑤 = ( 𝐺 ‘ 𝑥 ) ↔ ∀ 𝑦 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑥 ) ) )
36 18 35 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑤 ∈ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) 𝑤 = ( 𝐺 ‘ 𝑥 ) )
37 24 fdmd ⊢ ( 𝜑 → dom 𝐺 = 𝑋 )
38 37 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ dom 𝐺 ↔ 𝑥 ∈ 𝑋 ) )
39 38 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ dom 𝐺 )
40 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
41 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
42 fniniseg ⊢ ( 𝐹 Fn 𝑋 → ( 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
43 7 42 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) ) ) )
44 40 41 43 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
45 inelcm ⊢ ( ( 𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) → ( dom 𝐺 ∩ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ≠ ∅ )
46 39 44 45 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( dom 𝐺 ∩ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ≠ ∅ )
47 imadisj ⊢ ( ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) = ∅ ↔ ( dom 𝐺 ∩ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) = ∅ )
48 47 necon3bii ⊢ ( ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ≠ ∅ ↔ ( dom 𝐺 ∩ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ≠ ∅ )
49 46 48 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ≠ ∅ )
50 eqsn ⊢ ( ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ≠ ∅ → ( ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) = { ( 𝐺 ‘ 𝑥 ) } ↔ ∀ 𝑤 ∈ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) 𝑤 = ( 𝐺 ‘ 𝑥 ) ) )
51 49 50 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) = { ( 𝐺 ‘ 𝑥 ) } ↔ ∀ 𝑤 ∈ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) 𝑤 = ( 𝐺 ‘ 𝑥 ) ) )
52 36 51 mpbird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) = { ( 𝐺 ‘ 𝑥 ) } )
53 52 unieqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) = ∪ { ( 𝐺 ‘ 𝑥 ) } )
54 fvex ⊢ ( 𝐺 ‘ 𝑥 ) ∈ V
55 54 unisn ⊢ ∪ { ( 𝐺 ‘ 𝑥 ) } = ( 𝐺 ‘ 𝑥 )
56 53 55 eqtr2di ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) = ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
57 56 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) = ( 𝑥 ∈ 𝑋 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ) )
58 24 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐺 ‘ 𝑥 ) ) )
59 29 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑌 )
60 29 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) )
61 eqidd ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) = ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) )
62 sneq ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑥 ) → { 𝑤 } = { ( 𝐹 ‘ 𝑥 ) } )
63 62 imaeq2d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑥 ) → ( ◡ 𝐹 “ { 𝑤 } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) )
64 63 imaeq2d ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑥 ) → ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) = ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
65 64 unieqd ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑥 ) → ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) = ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) )
66 59 60 61 65 fmptco ⊢ ( 𝜑 → ( ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) ∘ 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ) )
67 57 58 66 3eqtr4d ⊢ ( 𝜑 → 𝐺 = ( ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) ∘ 𝐹 ) )
68 67 3 eqeltrrd ⊢ ( 𝜑 → ( ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) )
69 24 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 ‘ 𝑥 ) ∈ ∪ 𝐾 )
70 56 69 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ∈ ∪ 𝐾 )
71 70 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ∈ ∪ 𝐾 )
72 65 eqcomd ⊢ ( 𝑤 = ( 𝐹 ‘ 𝑥 ) → ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) = ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) )
73 72 eqcoms ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑤 → ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) = ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) )
74 73 eleq1d ⊢ ( ( 𝐹 ‘ 𝑥 ) = 𝑤 → ( ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ∈ ∪ 𝐾 ↔ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ∈ ∪ 𝐾 ) )
75 74 cbvfo ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → ( ∀ 𝑥 ∈ 𝑋 ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ∈ ∪ 𝐾 ↔ ∀ 𝑤 ∈ 𝑌 ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ∈ ∪ 𝐾 ) )
76 2 75 syl ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑋 ∪ ( 𝐺 “ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝑥 ) } ) ) ∈ ∪ 𝐾 ↔ ∀ 𝑤 ∈ 𝑌 ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ∈ ∪ 𝐾 ) )
77 71 76 mpbid ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑌 ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ∈ ∪ 𝐾 )
78 eqid ⊢ ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) = ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) )
79 78 fmpt ⊢ ( ∀ 𝑤 ∈ 𝑌 ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ∈ ∪ 𝐾 ↔ ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) : 𝑌 ⟶ ∪ 𝐾 )
80 77 79 sylib ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) : 𝑌 ⟶ ∪ 𝐾 )
81 qtopcn ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ) ∧ ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) : 𝑌 ⟶ ∪ 𝐾 ) ) → ( ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ↔ ( ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
82 1 22 2 80 81 syl22anc ⊢ ( 𝜑 → ( ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ↔ ( ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) ∘ 𝐹 ) ∈ ( 𝐽 Cn 𝐾 ) ) )
83 68 82 mpbird ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) )
84 coeq1 ⊢ ( 𝑓 = ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) → ( 𝑓 ∘ 𝐹 ) = ( ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) ∘ 𝐹 ) )
85 84 rspceeqv ⊢ ( ( ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝐺 = ( ( 𝑤 ∈ 𝑌 ↦ ∪ ( 𝐺 “ ( ◡ 𝐹 “ { 𝑤 } ) ) ) ∘ 𝐹 ) ) → ∃ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) 𝐺 = ( 𝑓 ∘ 𝐹 ) )
86 83 67 85 syl2anc ⊢ ( 𝜑 → ∃ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) 𝐺 = ( 𝑓 ∘ 𝐹 ) )
87 eqtr2 ⊢ ( ( 𝐺 = ( 𝑓 ∘ 𝐹 ) ∧ 𝐺 = ( 𝑔 ∘ 𝐹 ) ) → ( 𝑓 ∘ 𝐹 ) = ( 𝑔 ∘ 𝐹 ) )
88 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) ) → 𝐹 : 𝑋 –onto→ 𝑌 )
89 qtoptopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐹 : 𝑋 –onto→ 𝑌 ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
90 1 2 89 syl2anc ⊢ ( 𝜑 → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
91 90 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) ) → ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) )
92 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
93 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) ) → 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) )
94 cnf2 ⊢ ( ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) → 𝑓 : 𝑌 ⟶ ∪ 𝐾 )
95 91 92 93 94 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) ) → 𝑓 : 𝑌 ⟶ ∪ 𝐾 )
96 95 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) ) → 𝑓 Fn 𝑌 )
97 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) ) → 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) )
98 cnf2 ⊢ ( ( ( 𝐽 qTop 𝐹 ) ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) → 𝑔 : 𝑌 ⟶ ∪ 𝐾 )
99 91 92 97 98 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) ) → 𝑔 : 𝑌 ⟶ ∪ 𝐾 )
100 99 ffnd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) ) → 𝑔 Fn 𝑌 )
101 cocan2 ⊢ ( ( 𝐹 : 𝑋 –onto→ 𝑌 ∧ 𝑓 Fn 𝑌 ∧ 𝑔 Fn 𝑌 ) → ( ( 𝑓 ∘ 𝐹 ) = ( 𝑔 ∘ 𝐹 ) ↔ 𝑓 = 𝑔 ) )
102 88 96 100 101 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) ) → ( ( 𝑓 ∘ 𝐹 ) = ( 𝑔 ∘ 𝐹 ) ↔ 𝑓 = 𝑔 ) )
103 87 102 imbitrid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∧ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ) ) → ( ( 𝐺 = ( 𝑓 ∘ 𝐹 ) ∧ 𝐺 = ( 𝑔 ∘ 𝐹 ) ) → 𝑓 = 𝑔 ) )
104 103 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∀ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ( ( 𝐺 = ( 𝑓 ∘ 𝐹 ) ∧ 𝐺 = ( 𝑔 ∘ 𝐹 ) ) → 𝑓 = 𝑔 ) )
105 coeq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∘ 𝐹 ) = ( 𝑔 ∘ 𝐹 ) )
106 105 eqeq2d ⊢ ( 𝑓 = 𝑔 → ( 𝐺 = ( 𝑓 ∘ 𝐹 ) ↔ 𝐺 = ( 𝑔 ∘ 𝐹 ) ) )
107 106 reu4 ⊢ ( ∃! 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) 𝐺 = ( 𝑓 ∘ 𝐹 ) ↔ ( ∃ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) 𝐺 = ( 𝑓 ∘ 𝐹 ) ∧ ∀ 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ∀ 𝑔 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) ( ( 𝐺 = ( 𝑓 ∘ 𝐹 ) ∧ 𝐺 = ( 𝑔 ∘ 𝐹 ) ) → 𝑓 = 𝑔 ) ) )
108 86 104 107 sylanbrc ⊢ ( 𝜑 → ∃! 𝑓 ∈ ( ( 𝐽 qTop 𝐹 ) Cn 𝐾 ) 𝐺 = ( 𝑓 ∘ 𝐹 ) )