Metamath Proof Explorer

Theorem uptr2

Description: Universal property and fully faithful functor surjective on objects. (Contributed by Zhi Wang, 25-Nov-2025)

Ref Expression
Hypotheses uptr2.a ⊢ 𝐴 = ( Base ‘ 𝐶 )
uptr2.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
uptr2.y ⊢ ( 𝜑 → 𝑌 = ( 𝑅 ‘ 𝑋 ) )
uptr2.r ⊢ ( 𝜑 → 𝑅 : 𝐴 –onto→ 𝐵 )
uptr2.s ⊢ ( 𝜑 → 𝑅 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝑆 )
uptr2.f ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝑅 , 𝑆 ⟩ ) = ⟨ 𝐹 , 𝐺 ⟩ )
uptr2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
uptr2.k ⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
Assertion uptr2 ( 𝜑 → ( 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐸 ) 𝑍 ) 𝑀 ↔ 𝑌 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 ) )

Proof

Step Hyp Ref Expression
1 uptr2.a ⊢ 𝐴 = ( Base ‘ 𝐶 )
2 uptr2.b ⊢ 𝐵 = ( Base ‘ 𝐷 )
3 uptr2.y ⊢ ( 𝜑 → 𝑌 = ( 𝑅 ‘ 𝑋 ) )
4 uptr2.r ⊢ ( 𝜑 → 𝑅 : 𝐴 –onto→ 𝐵 )
5 uptr2.s ⊢ ( 𝜑 → 𝑅 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝑆 )
6 uptr2.f ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝑅 , 𝑆 ⟩ ) = ⟨ 𝐹 , 𝐺 ⟩ )
7 uptr2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
8 uptr2.k ⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐸 ) 𝑍 ) 𝑀 ) → 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐸 ) 𝑍 ) 𝑀 )
10 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
11 9 10 uprcl3 ⊢ ( ( 𝜑 ∧ 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐸 ) 𝑍 ) 𝑀 ) → 𝑍 ∈ ( Base ‘ 𝐸 ) )
12 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
13 9 12 uprcl5 ⊢ ( ( 𝜑 ∧ 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐸 ) 𝑍 ) 𝑀 ) → 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
14 11 13 jca ⊢ ( ( 𝜑 ∧ 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐸 ) 𝑍 ) 𝑀 ) → ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 ) → 𝑌 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 )
16 15 10 uprcl3 ⊢ ( ( 𝜑 ∧ 𝑌 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 ) → 𝑍 ∈ ( Base ‘ 𝐸 ) )
17 15 12 uprcl5 ⊢ ( ( 𝜑 ∧ 𝑌 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 ) → 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑌 ) ) )
18 3 fveq2d ⊢ ( 𝜑 → ( 𝐾 ‘ 𝑌 ) = ( 𝐾 ‘ ( 𝑅 ‘ 𝑋 ) ) )
19 inss1 ⊢ ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) ⊆ ( 𝐶 Full 𝐷 )
20 fullfunc ⊢ ( 𝐶 Full 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
21 19 20 sstri ⊢ ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) ⊆ ( 𝐶 Func 𝐷 )
22 21 ssbri ⊢ ( 𝑅 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝑆 → 𝑅 ( 𝐶 Func 𝐷 ) 𝑆 )
23 5 22 syl ⊢ ( 𝜑 → 𝑅 ( 𝐶 Func 𝐷 ) 𝑆 )
24 1 23 8 6 7 cofu1a ⊢ ( 𝜑 → ( 𝐾 ‘ ( 𝑅 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
25 18 24 eqtrd ⊢ ( 𝜑 → ( 𝐾 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) )
26 25 oveq2d ⊢ ( 𝜑 → ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑌 ) ) = ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 ) → ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑌 ) ) = ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
28 17 27 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑌 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 ) → 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
29 16 28 jca ⊢ ( ( 𝜑 ∧ 𝑌 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 ) → ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) )
30 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → 𝑅 : 𝐴 –onto→ 𝐵 )
31 fof ⊢ ( 𝑅 : 𝐴 –onto→ 𝐵 → 𝑅 : 𝐴 ⟶ 𝐵 )
32 30 31 syl ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → 𝑅 : 𝐴 ⟶ 𝐵 )
33 32 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑅 ‘ 𝑥 ) ∈ 𝐵 )
34 foelrn ⊢ ( ( 𝑅 : 𝐴 –onto→ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝑅 ‘ 𝑥 ) )
35 30 34 sylan ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑦 = ( 𝑅 ‘ 𝑥 ) )
36 simp3 ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → 𝑦 = ( 𝑅 ‘ 𝑥 ) )
37 36 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( 𝐾 ‘ 𝑦 ) = ( 𝐾 ‘ ( 𝑅 ‘ 𝑥 ) ) )
38 simp1l ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → 𝜑 )
39 38 23 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → 𝑅 ( 𝐶 Func 𝐷 ) 𝑆 )
40 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
41 40 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
42 38 6 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝑅 , 𝑆 ⟩ ) = ⟨ 𝐹 , 𝐺 ⟩ )
43 simp2 ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → 𝑥 ∈ 𝐴 )
44 1 39 41 42 43 cofu1a ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( 𝐾 ‘ ( 𝑅 ‘ 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
45 37 44 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( 𝐾 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
46 45 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) = ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) )
47 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
48 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
49 38 5 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → 𝑅 ( ( 𝐶 Full 𝐷 ) ∩ ( 𝐶 Faith 𝐷 ) ) 𝑆 )
50 38 7 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → 𝑋 ∈ 𝐴 )
51 1 47 48 49 50 43 ffthf1o ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( 𝑋 𝑆 𝑥 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) –1-1-onto→ ( ( 𝑅 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑅 ‘ 𝑥 ) ) )
52 38 3 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → 𝑌 = ( 𝑅 ‘ 𝑋 ) )
53 52 36 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) = ( ( 𝑅 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑅 ‘ 𝑥 ) ) )
54 53 f1oeq3d ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( ( 𝑋 𝑆 𝑥 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) –1-1-onto→ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) ↔ ( 𝑋 𝑆 𝑥 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) –1-1-onto→ ( ( 𝑅 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝑅 ‘ 𝑥 ) ) ) )
55 51 54 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( 𝑋 𝑆 𝑥 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) –1-1-onto→ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) )
56 f1of ⊢ ( ( 𝑋 𝑆 𝑥 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) –1-1-onto→ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) → ( 𝑋 𝑆 𝑥 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ⟶ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) )
57 55 56 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( 𝑋 𝑆 𝑥 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ⟶ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) )
58 57 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) )
59 f1ofveu ⊢ ( ( ( 𝑋 𝑆 𝑥 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) –1-1-onto→ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑙 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) ) → ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) = 𝑙 )
60 eqcom ⊢ ( ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) = 𝑙 ↔ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) )
61 60 reubii ⊢ ( ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) = 𝑙 ↔ ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) )
62 59 61 sylib ⊢ ( ( ( 𝑋 𝑆 𝑥 ) : ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) –1-1-onto→ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) ∧ 𝑙 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) ) → ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) )
63 55 62 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ 𝑙 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) ) → ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) )
64 38 25 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( 𝐾 ‘ 𝑌 ) = ( 𝐹 ‘ 𝑋 ) )
65 64 opeq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ⟨ 𝑍 , ( 𝐾 ‘ 𝑌 ) ⟩ = ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ )
66 65 45 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( ⟨ 𝑍 , ( 𝐾 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) = ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) )
67 66 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → ( ⟨ 𝑍 , ( 𝐾 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) = ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) )
68 52 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → 𝑌 = ( 𝑅 ‘ 𝑋 ) )
69 simpl3 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → 𝑦 = ( 𝑅 ‘ 𝑥 ) )
70 68 69 oveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → ( 𝑌 𝐿 𝑦 ) = ( ( 𝑅 ‘ 𝑋 ) 𝐿 ( 𝑅 ‘ 𝑥 ) ) )
71 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) )
72 70 71 fveq12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → ( ( 𝑌 𝐿 𝑦 ) ‘ 𝑙 ) = ( ( ( 𝑅 ‘ 𝑋 ) 𝐿 ( 𝑅 ‘ 𝑥 ) ) ‘ ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) )
73 39 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → 𝑅 ( 𝐶 Func 𝐷 ) 𝑆 )
74 41 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
75 42 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝑅 , 𝑆 ⟩ ) = ⟨ 𝐹 , 𝐺 ⟩ )
76 50 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → 𝑋 ∈ 𝐴 )
77 43 adantr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → 𝑥 ∈ 𝐴 )
78 simprl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) )
79 1 73 74 75 76 77 47 78 cofu2a ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → ( ( ( 𝑅 ‘ 𝑋 ) 𝐿 ( 𝑅 ‘ 𝑥 ) ) ‘ ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) = ( ( 𝑋 𝐺 𝑥 ) ‘ 𝑘 ) )
80 72 79 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → ( ( 𝑌 𝐿 𝑦 ) ‘ 𝑙 ) = ( ( 𝑋 𝐺 𝑥 ) ‘ 𝑘 ) )
81 eqidd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → 𝑀 = 𝑀 )
82 67 80 81 oveq123d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → ( ( ( 𝑌 𝐿 𝑦 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐾 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) 𝑀 ) = ( ( ( 𝑋 𝐺 𝑥 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) 𝑀 ) )
83 82 eqeq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) ∧ ( 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) ∧ 𝑙 = ( ( 𝑋 𝑆 𝑥 ) ‘ 𝑘 ) ) ) → ( 𝑔 = ( ( ( 𝑌 𝐿 𝑦 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐾 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) 𝑀 ) ↔ 𝑔 = ( ( ( 𝑋 𝐺 𝑥 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) 𝑀 ) ) )
84 58 63 83 reuxfr1dd ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( ∃! 𝑙 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) 𝑔 = ( ( ( 𝑌 𝐿 𝑦 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐾 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) 𝑀 ) ↔ ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑔 = ( ( ( 𝑋 𝐺 𝑥 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) 𝑀 ) ) )
85 46 84 raleqbidv ⊢ ( ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = ( 𝑅 ‘ 𝑥 ) ) → ( ∀ 𝑔 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) ∃! 𝑙 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) 𝑔 = ( ( ( 𝑌 𝐿 𝑦 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐾 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) 𝑀 ) ↔ ∀ 𝑔 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑔 = ( ( ( 𝑋 𝐺 𝑥 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) 𝑀 ) ) )
86 33 35 85 ralxfrd2 ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → ( ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) ∃! 𝑙 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) 𝑔 = ( ( ( 𝑌 𝐿 𝑦 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐾 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) 𝑀 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑔 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑔 = ( ( ( 𝑋 𝐺 𝑥 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) 𝑀 ) ) )
87 eqid ⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
88 simprl ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → 𝑍 ∈ ( Base ‘ 𝐸 ) )
89 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → 𝑌 = ( 𝑅 ‘ 𝑋 ) )
90 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → 𝑋 ∈ 𝐴 )
91 32 90 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → ( 𝑅 ‘ 𝑋 ) ∈ 𝐵 )
92 89 91 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → 𝑌 ∈ 𝐵 )
93 simprr ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
94 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑌 ) ) = ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
95 93 94 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑌 ) ) )
96 2 10 48 12 87 88 40 92 95 isup ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → ( 𝑌 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 ↔ ∀ 𝑦 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) ∃! 𝑙 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) 𝑔 = ( ( ( 𝑌 𝐿 𝑦 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐾 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐾 ‘ 𝑦 ) ) 𝑀 ) ) )
97 23 8 cofucla ⊢ ( 𝜑 → ( ⟨ 𝐾 , 𝐿 ⟩ ∘func ⟨ 𝑅 , 𝑆 ⟩ ) ∈ ( 𝐶 Func 𝐸 ) )
98 6 97 eqeltrrd ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐸 ) )
99 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐸 ) )
100 98 99 sylibr ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 )
101 100 adantr ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → 𝐹 ( 𝐶 Func 𝐸 ) 𝐺 )
102 1 10 47 12 87 88 101 90 93 isup ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → ( 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐸 ) 𝑍 ) 𝑀 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑔 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑔 = ( ( ( 𝑋 𝐺 𝑥 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) 𝑀 ) ) )
103 86 96 102 3bitr4rd ⊢ ( ( 𝜑 ∧ ( 𝑍 ∈ ( Base ‘ 𝐸 ) ∧ 𝑀 ∈ ( 𝑍 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ) ) → ( 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐸 ) 𝑍 ) 𝑀 ↔ 𝑌 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 ) )
104 14 29 103 bibiad ⊢ ( 𝜑 → ( 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 UP 𝐸 ) 𝑍 ) 𝑀 ↔ 𝑌 ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 UP 𝐸 ) 𝑍 ) 𝑀 ) )