Metamath Proof Explorer

Theorem catcisolem

Description: Lemma for catciso . (Contributed by Mario Carneiro, 29-Jan-2017)

Ref Expression
Hypotheses catciso.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
catciso.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
catciso.r ⊢ 𝑅 = ( Base ‘ 𝑋 )
catciso.s ⊢ 𝑆 = ( Base ‘ 𝑌 )
catciso.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
catciso.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
catciso.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
catcisolem.i ⊢ 𝐼 = ( Inv ‘ 𝐶 )
catcisolem.g ⊢ 𝐻 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ◡ ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) )
catcisolem.1 ⊢ ( 𝜑 → 𝐹 ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) 𝐺 )
catcisolem.2 ⊢ ( 𝜑 → 𝐹 : 𝑅 –1-1-onto→ 𝑆 )
Assertion catcisolem ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ( 𝑋 𝐼 𝑌 ) ⟨ ◡ 𝐹 , 𝐻 ⟩ )

Proof

Step Hyp Ref Expression
1 catciso.c ⊢ 𝐶 = ( CatCat ‘ 𝑈 )
2 catciso.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 catciso.r ⊢ 𝑅 = ( Base ‘ 𝑋 )
4 catciso.s ⊢ 𝑆 = ( Base ‘ 𝑌 )
5 catciso.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
6 catciso.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
7 catciso.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
8 catcisolem.i ⊢ 𝐼 = ( Inv ‘ 𝐶 )
9 catcisolem.g ⊢ 𝐻 = ( 𝑥 ∈ 𝑆 , 𝑦 ∈ 𝑆 ↦ ◡ ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) )
10 catcisolem.1 ⊢ ( 𝜑 → 𝐹 ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) 𝐺 )
11 catcisolem.2 ⊢ ( 𝜑 → 𝐹 : 𝑅 –1-1-onto→ 𝑆 )
12 f1ococnv1 ⊢ ( 𝐹 : 𝑅 –1-1-onto→ 𝑆 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝑅 ) )
13 11 12 syl ⊢ ( 𝜑 → ( ◡ 𝐹 ∘ 𝐹 ) = ( I ↾ 𝑅 ) )
14 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → 𝐹 : 𝑅 –1-1-onto→ 𝑆 )
15 f1of ⊢ ( 𝐹 : 𝑅 –1-1-onto→ 𝑆 → 𝐹 : 𝑅 ⟶ 𝑆 )
16 14 15 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → 𝐹 : 𝑅 ⟶ 𝑆 )
17 simp2 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → 𝑢 ∈ 𝑅 )
18 16 17 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ( 𝐹 ‘ 𝑢 ) ∈ 𝑆 )
19 simp3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → 𝑣 ∈ 𝑅 )
20 16 19 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 )
21 simpl ⊢ ( ( 𝑥 = ( 𝐹 ‘ 𝑢 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑣 ) ) → 𝑥 = ( 𝐹 ‘ 𝑢 ) )
22 21 fveq2d ⊢ ( ( 𝑥 = ( 𝐹 ‘ 𝑢 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑣 ) ) → ( ◡ 𝐹 ‘ 𝑥 ) = ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) )
23 simpr ⊢ ( ( 𝑥 = ( 𝐹 ‘ 𝑢 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑣 ) ) → 𝑦 = ( 𝐹 ‘ 𝑣 ) )
24 23 fveq2d ⊢ ( ( 𝑥 = ( 𝐹 ‘ 𝑢 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑣 ) ) → ( ◡ 𝐹 ‘ 𝑦 ) = ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑣 ) ) )
25 22 24 oveq12d ⊢ ( ( 𝑥 = ( 𝐹 ‘ 𝑢 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑣 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) = ( ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) 𝐺 ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑣 ) ) ) )
26 25 cnveqd ⊢ ( ( 𝑥 = ( 𝐹 ‘ 𝑢 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑣 ) ) → ◡ ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) = ◡ ( ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) 𝐺 ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑣 ) ) ) )
27 ovex ⊢ ( ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) 𝐺 ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑣 ) ) ) ∈ V
28 27 cnvex ⊢ ◡ ( ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) 𝐺 ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑣 ) ) ) ∈ V
29 26 9 28 ovmpoa ⊢ ( ( ( 𝐹 ‘ 𝑢 ) ∈ 𝑆 ∧ ( 𝐹 ‘ 𝑣 ) ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑢 ) 𝐻 ( 𝐹 ‘ 𝑣 ) ) = ◡ ( ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) 𝐺 ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑣 ) ) ) )
30 18 20 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ( ( 𝐹 ‘ 𝑢 ) 𝐻 ( 𝐹 ‘ 𝑣 ) ) = ◡ ( ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) 𝐺 ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑣 ) ) ) )
31 f1ocnvfv1 ⊢ ( ( 𝐹 : 𝑅 –1-1-onto→ 𝑆 ∧ 𝑢 ∈ 𝑅 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) = 𝑢 )
32 14 17 31 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) = 𝑢 )
33 f1ocnvfv1 ⊢ ( ( 𝐹 : 𝑅 –1-1-onto→ 𝑆 ∧ 𝑣 ∈ 𝑅 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑣 ) ) = 𝑣 )
34 14 19 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑣 ) ) = 𝑣 )
35 32 34 oveq12d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ( ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) 𝐺 ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑣 ) ) ) = ( 𝑢 𝐺 𝑣 ) )
36 35 cnveqd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ◡ ( ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑢 ) ) 𝐺 ( ◡ 𝐹 ‘ ( 𝐹 ‘ 𝑣 ) ) ) = ◡ ( 𝑢 𝐺 𝑣 ) )
37 30 36 eqtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ( ( 𝐹 ‘ 𝑢 ) 𝐻 ( 𝐹 ‘ 𝑣 ) ) = ◡ ( 𝑢 𝐺 𝑣 ) )
38 37 coeq1d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ( ( ( 𝐹 ‘ 𝑢 ) 𝐻 ( 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐺 𝑣 ) ) = ( ◡ ( 𝑢 𝐺 𝑣 ) ∘ ( 𝑢 𝐺 𝑣 ) ) )
39 eqid ⊢ ( Hom ‘ 𝑋 ) = ( Hom ‘ 𝑋 )
40 eqid ⊢ ( Hom ‘ 𝑌 ) = ( Hom ‘ 𝑌 )
41 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → 𝐹 ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) 𝐺 )
42 3 39 40 41 17 19 ffthf1o ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ( 𝑢 𝐺 𝑣 ) : ( 𝑢 ( Hom ‘ 𝑋 ) 𝑣 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ 𝑣 ) ) )
43 f1ococnv1 ⊢ ( ( 𝑢 𝐺 𝑣 ) : ( 𝑢 ( Hom ‘ 𝑋 ) 𝑣 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ 𝑣 ) ) → ( ◡ ( 𝑢 𝐺 𝑣 ) ∘ ( 𝑢 𝐺 𝑣 ) ) = ( I ↾ ( 𝑢 ( Hom ‘ 𝑋 ) 𝑣 ) ) )
44 42 43 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ( ◡ ( 𝑢 𝐺 𝑣 ) ∘ ( 𝑢 𝐺 𝑣 ) ) = ( I ↾ ( 𝑢 ( Hom ‘ 𝑋 ) 𝑣 ) ) )
45 38 44 eqtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) → ( ( ( 𝐹 ‘ 𝑢 ) 𝐻 ( 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐺 𝑣 ) ) = ( I ↾ ( 𝑢 ( Hom ‘ 𝑋 ) 𝑣 ) ) )
46 45 mpoeq3dva ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑅 ↦ ( ( ( 𝐹 ‘ 𝑢 ) 𝐻 ( 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐺 𝑣 ) ) ) = ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑅 ↦ ( I ↾ ( 𝑢 ( Hom ‘ 𝑋 ) 𝑣 ) ) ) )
47 fveq2 ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( Hom ‘ 𝑋 ) ‘ 𝑧 ) = ( ( Hom ‘ 𝑋 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
48 df-ov ⊢ ( 𝑢 ( Hom ‘ 𝑋 ) 𝑣 ) = ( ( Hom ‘ 𝑋 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
49 47 48 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( Hom ‘ 𝑋 ) ‘ 𝑧 ) = ( 𝑢 ( Hom ‘ 𝑋 ) 𝑣 ) )
50 49 reseq2d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( I ↾ ( ( Hom ‘ 𝑋 ) ‘ 𝑧 ) ) = ( I ↾ ( 𝑢 ( Hom ‘ 𝑋 ) 𝑣 ) ) )
51 50 mpompt ⊢ ( 𝑧 ∈ ( 𝑅 × 𝑅 ) ↦ ( I ↾ ( ( Hom ‘ 𝑋 ) ‘ 𝑧 ) ) ) = ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑅 ↦ ( I ↾ ( 𝑢 ( Hom ‘ 𝑋 ) 𝑣 ) ) )
52 46 51 eqtr4di ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑅 ↦ ( ( ( 𝐹 ‘ 𝑢 ) 𝐻 ( 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐺 𝑣 ) ) ) = ( 𝑧 ∈ ( 𝑅 × 𝑅 ) ↦ ( I ↾ ( ( Hom ‘ 𝑋 ) ‘ 𝑧 ) ) ) )
53 13 52 opeq12d ⊢ ( 𝜑 → ⟨ ( ◡ 𝐹 ∘ 𝐹 ) , ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑅 ↦ ( ( ( 𝐹 ‘ 𝑢 ) 𝐻 ( 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐺 𝑣 ) ) ) ⟩ = ⟨ ( I ↾ 𝑅 ) , ( 𝑧 ∈ ( 𝑅 × 𝑅 ) ↦ ( I ↾ ( ( Hom ‘ 𝑋 ) ‘ 𝑧 ) ) ) ⟩ )
54 inss1 ⊢ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ⊆ ( 𝑋 Full 𝑌 )
55 fullfunc ⊢ ( 𝑋 Full 𝑌 ) ⊆ ( 𝑋 Func 𝑌 )
56 54 55 sstri ⊢ ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) ⊆ ( 𝑋 Func 𝑌 )
57 56 ssbri ⊢ ( 𝐹 ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) 𝐺 → 𝐹 ( 𝑋 Func 𝑌 ) 𝐺 )
58 10 57 syl ⊢ ( 𝜑 → 𝐹 ( 𝑋 Func 𝑌 ) 𝐺 )
59 eqid ⊢ ( Id ‘ 𝑌 ) = ( Id ‘ 𝑌 )
60 eqid ⊢ ( Id ‘ 𝑋 ) = ( Id ‘ 𝑋 )
61 eqid ⊢ ( comp ‘ 𝑌 ) = ( comp ‘ 𝑌 )
62 eqid ⊢ ( comp ‘ 𝑋 ) = ( comp ‘ 𝑋 )
63 1 2 5 catcbas ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
64 inss2 ⊢ ( 𝑈 ∩ Cat ) ⊆ Cat
65 63 64 eqsstrdi ⊢ ( 𝜑 → 𝐵 ⊆ Cat )
66 65 7 sseldd ⊢ ( 𝜑 → 𝑌 ∈ Cat )
67 65 6 sseldd ⊢ ( 𝜑 → 𝑋 ∈ Cat )
68 f1ocnv ⊢ ( 𝐹 : 𝑅 –1-1-onto→ 𝑆 → ◡ 𝐹 : 𝑆 –1-1-onto→ 𝑅 )
69 f1of ⊢ ( ◡ 𝐹 : 𝑆 –1-1-onto→ 𝑅 → ◡ 𝐹 : 𝑆 ⟶ 𝑅 )
70 11 68 69 3syl ⊢ ( 𝜑 → ◡ 𝐹 : 𝑆 ⟶ 𝑅 )
71 ovex ⊢ ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ V
72 71 cnvex ⊢ ◡ ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) ∈ V
73 9 72 fnmpoi ⊢ 𝐻 Fn ( 𝑆 × 𝑆 )
74 73 a1i ⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
75 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → 𝐹 ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) 𝐺 )
76 70 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑅 )
77 76 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑅 )
78 70 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑆 ) → ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑅 )
79 78 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑅 )
80 3 39 40 75 77 79 ffthf1o ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) )
81 f1ocnv ⊢ ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) → ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) –1-1-onto→ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) )
82 f1of ⊢ ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) –1-1-onto→ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) → ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) ⟶ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) )
83 80 81 82 3syl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) ⟶ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) )
84 simpl ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑥 = 𝑢 )
85 84 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ◡ 𝐹 ‘ 𝑥 ) = ( ◡ 𝐹 ‘ 𝑢 ) )
86 simpr ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝑦 = 𝑣 )
87 86 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ◡ 𝐹 ‘ 𝑦 ) = ( ◡ 𝐹 ‘ 𝑣 ) )
88 85 87 oveq12d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) )
89 88 cnveqd ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → ◡ ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) = ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) )
90 ovex ⊢ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ∈ V
91 90 cnvex ⊢ ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ∈ V
92 89 9 91 ovmpoa ⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 𝐻 𝑣 ) = ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) )
93 92 adantl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( 𝑢 𝐻 𝑣 ) = ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) )
94 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → 𝐹 : 𝑅 –1-1-onto→ 𝑆 )
95 simprl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → 𝑢 ∈ 𝑆 )
96 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑅 –1-1-onto→ 𝑆 ∧ 𝑢 ∈ 𝑆 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) = 𝑢 )
97 94 95 96 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) = 𝑢 )
98 simprr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → 𝑣 ∈ 𝑆 )
99 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑅 –1-1-onto→ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) = 𝑣 )
100 94 98 99 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) = 𝑣 )
101 97 100 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) = ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) )
102 101 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) = ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) )
103 93 102 feq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( ( 𝑢 𝐻 𝑣 ) : ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ⟶ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) ↔ ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) ⟶ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) ) )
104 83 103 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) → ( 𝑢 𝐻 𝑣 ) : ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ⟶ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) )
105 simpr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → 𝑢 ∈ 𝑆 )
106 simpl ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → 𝑥 = 𝑢 )
107 106 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( ◡ 𝐹 ‘ 𝑥 ) = ( ◡ 𝐹 ‘ 𝑢 ) )
108 simpr ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → 𝑦 = 𝑢 )
109 108 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( ◡ 𝐹 ‘ 𝑦 ) = ( ◡ 𝐹 ‘ 𝑢 ) )
110 107 109 oveq12d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) )
111 110 cnveqd ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑢 ) → ◡ ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) = ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) )
112 ovex ⊢ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) ∈ V
113 112 cnvex ⊢ ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) ∈ V
114 111 9 113 ovmpoa ⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑢 ∈ 𝑆 ) → ( 𝑢 𝐻 𝑢 ) = ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) )
115 105 105 114 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( 𝑢 𝐻 𝑢 ) = ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) )
116 115 fveq1d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ( 𝑢 𝐻 𝑢 ) ‘ ( ( Id ‘ 𝑌 ) ‘ 𝑢 ) ) = ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) ‘ ( ( Id ‘ 𝑌 ) ‘ 𝑢 ) ) )
117 58 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → 𝐹 ( 𝑋 Func 𝑌 ) 𝐺 )
118 3 60 59 117 76 funcid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) ‘ ( ( Id ‘ 𝑋 ) ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ) = ( ( Id ‘ 𝑌 ) ‘ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ) )
119 11 96 sylan ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) = 𝑢 )
120 119 fveq2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ( Id ‘ 𝑌 ) ‘ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ) = ( ( Id ‘ 𝑌 ) ‘ 𝑢 ) )
121 118 120 eqtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) ‘ ( ( Id ‘ 𝑋 ) ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ) = ( ( Id ‘ 𝑌 ) ‘ 𝑢 ) )
122 10 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → 𝐹 ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) 𝐺 )
123 3 39 40 122 76 76 ffthf1o ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑢 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ) )
124 67 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → 𝑋 ∈ Cat )
125 3 39 60 124 76 catidcl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ( Id ‘ 𝑋 ) ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ∈ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑢 ) ) )
126 f1ocnvfv ⊢ ( ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑢 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ) ∧ ( ( Id ‘ 𝑋 ) ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ∈ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑢 ) ) ) → ( ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) ‘ ( ( Id ‘ 𝑋 ) ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ) = ( ( Id ‘ 𝑌 ) ‘ 𝑢 ) → ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) ‘ ( ( Id ‘ 𝑌 ) ‘ 𝑢 ) ) = ( ( Id ‘ 𝑋 ) ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ) )
127 123 125 126 syl2anc ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) ‘ ( ( Id ‘ 𝑋 ) ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ) = ( ( Id ‘ 𝑌 ) ‘ 𝑢 ) → ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) ‘ ( ( Id ‘ 𝑌 ) ‘ 𝑢 ) ) = ( ( Id ‘ 𝑋 ) ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ) )
128 121 127 mpd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑢 ) ) ‘ ( ( Id ‘ 𝑌 ) ‘ 𝑢 ) ) = ( ( Id ‘ 𝑋 ) ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) )
129 116 128 eqtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ) → ( ( 𝑢 𝐻 𝑢 ) ‘ ( ( Id ‘ 𝑌 ) ‘ 𝑢 ) ) = ( ( Id ‘ 𝑋 ) ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) )
130 58 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → 𝐹 ( 𝑋 Func 𝑌 ) 𝐺 )
131 70 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ◡ 𝐹 : 𝑆 ⟶ 𝑅 )
132 simp21 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → 𝑢 ∈ 𝑆 )
133 131 132 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑅 )
134 simp22 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → 𝑣 ∈ 𝑆 )
135 131 134 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑅 )
136 simp23 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → 𝑧 ∈ 𝑆 )
137 131 136 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ 𝑅 )
138 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → 𝐹 ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) 𝐺 )
139 3 39 40 138 133 135 ffthf1o ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) )
140 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → 𝐹 : 𝑅 –1-1-onto→ 𝑆 )
141 140 132 96 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) = 𝑢 )
142 140 134 99 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) = 𝑣 )
143 141 142 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) = ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) )
144 143 f1oeq3d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) ↔ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ) )
145 139 144 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) )
146 f1ocnv ⊢ ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) → ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) –1-1-onto→ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) )
147 f1of ⊢ ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) –1-1-onto→ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) → ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ⟶ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) )
148 145 146 147 3syl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ⟶ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) )
149 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) )
150 148 149 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ∈ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) )
151 3 39 40 138 135 137 ffthf1o ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( ( ◡ 𝐹 ‘ 𝑣 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ) )
152 f1ocnvfv2 ⊢ ( ( 𝐹 : 𝑅 –1-1-onto→ 𝑆 ∧ 𝑧 ∈ 𝑆 ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
153 140 136 152 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) = 𝑧 )
154 142 153 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ) = ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) )
155 154 f1oeq3d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( ( ◡ 𝐹 ‘ 𝑣 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ) ↔ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( ( ◡ 𝐹 ‘ 𝑣 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) –1-1-onto→ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) )
156 151 155 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( ( ◡ 𝐹 ‘ 𝑣 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) –1-1-onto→ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) )
157 f1ocnv ⊢ ( ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( ( ◡ 𝐹 ‘ 𝑣 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) –1-1-onto→ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) → ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) –1-1-onto→ ( ( ◡ 𝐹 ‘ 𝑣 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) )
158 f1of ⊢ ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) –1-1-onto→ ( ( ◡ 𝐹 ‘ 𝑣 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) → ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ⟶ ( ( ◡ 𝐹 ‘ 𝑣 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) )
159 156 157 158 3syl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ⟶ ( ( ◡ 𝐹 ‘ 𝑣 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) )
160 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) )
161 159 160 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ∈ ( ( ◡ 𝐹 ‘ 𝑣 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) )
162 3 39 62 61 130 133 135 137 150 161 funcco ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) ) = ( ( ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ) ( ⟨ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) , ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ⟩ ( comp ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ) ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) ) )
163 141 142 opeq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ⟨ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) , ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ⟩ = ⟨ 𝑢 , 𝑣 ⟩ )
164 163 153 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ⟨ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) , ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ⟩ ( comp ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ) = ( ⟨ 𝑢 , 𝑣 ⟩ ( comp ‘ 𝑌 ) 𝑧 ) )
165 f1ocnvfv2 ⊢ ( ( ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( ( ◡ 𝐹 ‘ 𝑣 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) –1-1-onto→ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ) = 𝑔 )
166 156 160 165 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ) = 𝑔 )
167 f1ocnvfv2 ⊢ ( ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) = 𝑓 )
168 145 149 167 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) = 𝑓 )
169 164 166 168 oveq123d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ) ( ⟨ ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) , ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ⟩ ( comp ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ) ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) ) = ( 𝑔 ( ⟨ 𝑢 , 𝑣 ⟩ ( comp ‘ 𝑌 ) 𝑧 ) 𝑓 ) )
170 162 169 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) ) = ( 𝑔 ( ⟨ 𝑢 , 𝑣 ⟩ ( comp ‘ 𝑌 ) 𝑧 ) 𝑓 ) )
171 3 39 40 138 133 137 ffthf1o ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ) )
172 141 153 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ) = ( 𝑢 ( Hom ‘ 𝑌 ) 𝑧 ) )
173 172 f1oeq3d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑧 ) ) ) ↔ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) –1-1-onto→ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑧 ) ) )
174 171 173 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) –1-1-onto→ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑧 ) )
175 67 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → 𝑋 ∈ Cat )
176 3 39 62 175 133 135 137 150 161 catcocl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) ∈ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) )
177 f1ocnvfv ⊢ ( ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) –1-1-onto→ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑧 ) ∧ ( ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) ∈ ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ) → ( ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) ) = ( 𝑔 ( ⟨ 𝑢 , 𝑣 ⟩ ( comp ‘ 𝑌 ) 𝑧 ) 𝑓 ) → ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑢 , 𝑣 ⟩ ( comp ‘ 𝑌 ) 𝑧 ) 𝑓 ) ) = ( ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) ) )
178 174 176 177 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) ) = ( 𝑔 ( ⟨ 𝑢 , 𝑣 ⟩ ( comp ‘ 𝑌 ) 𝑧 ) 𝑓 ) → ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑢 , 𝑣 ⟩ ( comp ‘ 𝑌 ) 𝑧 ) 𝑓 ) ) = ( ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) ) )
179 170 178 mpd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑢 , 𝑣 ⟩ ( comp ‘ 𝑌 ) 𝑧 ) 𝑓 ) ) = ( ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) )
180 simpl ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑧 ) → 𝑥 = 𝑢 )
181 180 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑧 ) → ( ◡ 𝐹 ‘ 𝑥 ) = ( ◡ 𝐹 ‘ 𝑢 ) )
182 simpr ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑧 ) → 𝑦 = 𝑧 )
183 182 fveq2d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑧 ) → ( ◡ 𝐹 ‘ 𝑦 ) = ( ◡ 𝐹 ‘ 𝑧 ) )
184 181 183 oveq12d ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑧 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) )
185 184 cnveqd ⊢ ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑧 ) → ◡ ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) = ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) )
186 ovex ⊢ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ V
187 186 cnvex ⊢ ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ V
188 185 9 187 ovmpoa ⊢ ( ( 𝑢 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) → ( 𝑢 𝐻 𝑧 ) = ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) )
189 132 136 188 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( 𝑢 𝐻 𝑧 ) = ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) )
190 189 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( 𝑢 𝐻 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑢 , 𝑣 ⟩ ( comp ‘ 𝑌 ) 𝑧 ) 𝑓 ) ) = ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ ( 𝑔 ( ⟨ 𝑢 , 𝑣 ⟩ ( comp ‘ 𝑌 ) 𝑧 ) 𝑓 ) ) )
191 simpl ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑧 ) → 𝑥 = 𝑣 )
192 191 fveq2d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑧 ) → ( ◡ 𝐹 ‘ 𝑥 ) = ( ◡ 𝐹 ‘ 𝑣 ) )
193 simpr ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑧 ) → 𝑦 = 𝑧 )
194 193 fveq2d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑧 ) → ( ◡ 𝐹 ‘ 𝑦 ) = ( ◡ 𝐹 ‘ 𝑧 ) )
195 192 194 oveq12d ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑧 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) = ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) )
196 195 cnveqd ⊢ ( ( 𝑥 = 𝑣 ∧ 𝑦 = 𝑧 ) → ◡ ( ( ◡ 𝐹 ‘ 𝑥 ) 𝐺 ( ◡ 𝐹 ‘ 𝑦 ) ) = ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) )
197 ovex ⊢ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ V
198 197 cnvex ⊢ ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ∈ V
199 196 9 198 ovmpoa ⊢ ( ( 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) → ( 𝑣 𝐻 𝑧 ) = ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) )
200 134 136 199 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( 𝑣 𝐻 𝑧 ) = ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) )
201 200 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( 𝑣 𝐻 𝑧 ) ‘ 𝑔 ) = ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) )
202 132 134 92 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( 𝑢 𝐻 𝑣 ) = ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) )
203 202 fveq1d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( 𝑢 𝐻 𝑣 ) ‘ 𝑓 ) = ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) )
204 201 203 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( ( 𝑣 𝐻 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ( 𝑢 𝐻 𝑣 ) ‘ 𝑓 ) ) = ( ( ◡ ( ( ◡ 𝐹 ‘ 𝑣 ) 𝐺 ( ◡ 𝐹 ‘ 𝑧 ) ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ‘ 𝑓 ) ) )
205 179 190 204 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom ‘ 𝑌 ) 𝑧 ) ) ) → ( ( 𝑢 𝐻 𝑧 ) ‘ ( 𝑔 ( ⟨ 𝑢 , 𝑣 ⟩ ( comp ‘ 𝑌 ) 𝑧 ) 𝑓 ) ) = ( ( ( 𝑣 𝐻 𝑧 ) ‘ 𝑔 ) ( ⟨ ( ◡ 𝐹 ‘ 𝑢 ) , ( ◡ 𝐹 ‘ 𝑣 ) ⟩ ( comp ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑧 ) ) ( ( 𝑢 𝐻 𝑣 ) ‘ 𝑓 ) ) )
206 4 3 40 39 59 60 61 62 66 67 70 74 104 129 205 isfuncd ⊢ ( 𝜑 → ◡ 𝐹 ( 𝑌 Func 𝑋 ) 𝐻 )
207 3 58 206 cofuval2 ⊢ ( 𝜑 → ( ⟨ ◡ 𝐹 , 𝐻 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ⟨ ( ◡ 𝐹 ∘ 𝐹 ) , ( 𝑢 ∈ 𝑅 , 𝑣 ∈ 𝑅 ↦ ( ( ( 𝐹 ‘ 𝑢 ) 𝐻 ( 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐺 𝑣 ) ) ) ⟩ )
208 eqid ⊢ ( idfunc ‘ 𝑋 ) = ( idfunc ‘ 𝑋 )
209 208 3 67 39 idfuval ⊢ ( 𝜑 → ( idfunc ‘ 𝑋 ) = ⟨ ( I ↾ 𝑅 ) , ( 𝑧 ∈ ( 𝑅 × 𝑅 ) ↦ ( I ↾ ( ( Hom ‘ 𝑋 ) ‘ 𝑧 ) ) ) ⟩ )
210 53 207 209 3eqtr4d ⊢ ( 𝜑 → ( ⟨ ◡ 𝐹 , 𝐻 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) = ( idfunc ‘ 𝑋 ) )
211 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
212 df-br ⊢ ( 𝐹 ( 𝑋 Func 𝑌 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 Func 𝑌 ) )
213 58 212 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 Func 𝑌 ) )
214 df-br ⊢ ( ◡ 𝐹 ( 𝑌 Func 𝑋 ) 𝐻 ↔ ⟨ ◡ 𝐹 , 𝐻 ⟩ ∈ ( 𝑌 Func 𝑋 ) )
215 206 214 sylib ⊢ ( 𝜑 → ⟨ ◡ 𝐹 , 𝐻 ⟩ ∈ ( 𝑌 Func 𝑋 ) )
216 1 2 5 211 6 7 6 213 215 catcco ⊢ ( 𝜑 → ( ⟨ ◡ 𝐹 , 𝐻 ⟩ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟨ 𝐹 , 𝐺 ⟩ ) = ( ⟨ ◡ 𝐹 , 𝐻 ⟩ ∘func ⟨ 𝐹 , 𝐺 ⟩ ) )
217 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
218 1 2 217 208 5 6 catcid ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) = ( idfunc ‘ 𝑋 ) )
219 210 216 218 3eqtr4d ⊢ ( 𝜑 → ( ⟨ ◡ 𝐹 , 𝐻 ⟩ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟨ 𝐹 , 𝐺 ⟩ ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) )
220 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
221 eqid ⊢ ( Sect ‘ 𝐶 ) = ( Sect ‘ 𝐶 )
222 1 catccat ⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ Cat )
223 5 222 syl ⊢ ( 𝜑 → 𝐶 ∈ Cat )
224 1 2 5 220 6 7 catchom ⊢ ( 𝜑 → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) = ( 𝑋 Func 𝑌 ) )
225 213 224 eleqtrrd ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑌 ) )
226 1 2 5 220 7 6 catchom ⊢ ( 𝜑 → ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) = ( 𝑌 Func 𝑋 ) )
227 215 226 eleqtrrd ⊢ ( 𝜑 → ⟨ ◡ 𝐹 , 𝐻 ⟩ ∈ ( 𝑌 ( Hom ‘ 𝐶 ) 𝑋 ) )
228 2 220 211 217 221 223 6 7 225 227 issect2 ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ⟨ ◡ 𝐹 , 𝐻 ⟩ ↔ ( ⟨ ◡ 𝐹 , 𝐻 ⟩ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟨ 𝐹 , 𝐺 ⟩ ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
229 219 228 mpbird ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ⟨ ◡ 𝐹 , 𝐻 ⟩ )
230 f1ococnv2 ⊢ ( 𝐹 : 𝑅 –1-1-onto→ 𝑆 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ 𝑆 ) )
231 11 230 syl ⊢ ( 𝜑 → ( 𝐹 ∘ ◡ 𝐹 ) = ( I ↾ 𝑆 ) )
232 92 3adant1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( 𝑢 𝐻 𝑣 ) = ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) )
233 232 coeq2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐻 𝑣 ) ) = ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ∘ ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ) )
234 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → 𝐹 ( ( 𝑋 Full 𝑌 ) ∩ ( 𝑋 Faith 𝑌 ) ) 𝐺 )
235 76 3adant3 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( ◡ 𝐹 ‘ 𝑢 ) ∈ 𝑅 )
236 78 3adant2 ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( ◡ 𝐹 ‘ 𝑣 ) ∈ 𝑅 )
237 3 39 40 234 235 236 ffthf1o ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) )
238 101 3impb ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) = ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) )
239 238 f1oeq3d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑢 ) ) ( Hom ‘ 𝑌 ) ( 𝐹 ‘ ( ◡ 𝐹 ‘ 𝑣 ) ) ) ↔ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ) )
240 237 239 mpbid ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) )
241 f1ococnv2 ⊢ ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) : ( ( ◡ 𝐹 ‘ 𝑢 ) ( Hom ‘ 𝑋 ) ( ◡ 𝐹 ‘ 𝑣 ) ) –1-1-onto→ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ∘ ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ) = ( I ↾ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ) )
242 240 241 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ∘ ◡ ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ) = ( I ↾ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ) )
243 233 242 eqtrd ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) → ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐻 𝑣 ) ) = ( I ↾ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ) )
244 243 mpoeq3dva ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 , 𝑣 ∈ 𝑆 ↦ ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐻 𝑣 ) ) ) = ( 𝑢 ∈ 𝑆 , 𝑣 ∈ 𝑆 ↦ ( I ↾ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ) ) )
245 fveq2 ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( Hom ‘ 𝑌 ) ‘ 𝑧 ) = ( ( Hom ‘ 𝑌 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ ) )
246 df-ov ⊢ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) = ( ( Hom ‘ 𝑌 ) ‘ ⟨ 𝑢 , 𝑣 ⟩ )
247 245 246 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( Hom ‘ 𝑌 ) ‘ 𝑧 ) = ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) )
248 247 reseq2d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( I ↾ ( ( Hom ‘ 𝑌 ) ‘ 𝑧 ) ) = ( I ↾ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ) )
249 248 mpompt ⊢ ( 𝑧 ∈ ( 𝑆 × 𝑆 ) ↦ ( I ↾ ( ( Hom ‘ 𝑌 ) ‘ 𝑧 ) ) ) = ( 𝑢 ∈ 𝑆 , 𝑣 ∈ 𝑆 ↦ ( I ↾ ( 𝑢 ( Hom ‘ 𝑌 ) 𝑣 ) ) )
250 244 249 eqtr4di ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑆 , 𝑣 ∈ 𝑆 ↦ ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐻 𝑣 ) ) ) = ( 𝑧 ∈ ( 𝑆 × 𝑆 ) ↦ ( I ↾ ( ( Hom ‘ 𝑌 ) ‘ 𝑧 ) ) ) )
251 231 250 opeq12d ⊢ ( 𝜑 → ⟨ ( 𝐹 ∘ ◡ 𝐹 ) , ( 𝑢 ∈ 𝑆 , 𝑣 ∈ 𝑆 ↦ ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐻 𝑣 ) ) ) ⟩ = ⟨ ( I ↾ 𝑆 ) , ( 𝑧 ∈ ( 𝑆 × 𝑆 ) ↦ ( I ↾ ( ( Hom ‘ 𝑌 ) ‘ 𝑧 ) ) ) ⟩ )
252 4 206 58 cofuval2 ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∘func ⟨ ◡ 𝐹 , 𝐻 ⟩ ) = ⟨ ( 𝐹 ∘ ◡ 𝐹 ) , ( 𝑢 ∈ 𝑆 , 𝑣 ∈ 𝑆 ↦ ( ( ( ◡ 𝐹 ‘ 𝑢 ) 𝐺 ( ◡ 𝐹 ‘ 𝑣 ) ) ∘ ( 𝑢 𝐻 𝑣 ) ) ) ⟩ )
253 eqid ⊢ ( idfunc ‘ 𝑌 ) = ( idfunc ‘ 𝑌 )
254 253 4 66 40 idfuval ⊢ ( 𝜑 → ( idfunc ‘ 𝑌 ) = ⟨ ( I ↾ 𝑆 ) , ( 𝑧 ∈ ( 𝑆 × 𝑆 ) ↦ ( I ↾ ( ( Hom ‘ 𝑌 ) ‘ 𝑧 ) ) ) ⟩ )
255 251 252 254 3eqtr4d ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∘func ⟨ ◡ 𝐹 , 𝐻 ⟩ ) = ( idfunc ‘ 𝑌 ) )
256 1 2 5 211 7 6 7 215 213 catcco ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ⟨ ◡ 𝐹 , 𝐻 ⟩ ) = ( ⟨ 𝐹 , 𝐺 ⟩ ∘func ⟨ ◡ 𝐹 , 𝐻 ⟩ ) )
257 1 2 217 253 5 7 catcid ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) = ( idfunc ‘ 𝑌 ) )
258 255 256 257 3eqtr4d ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ⟨ ◡ 𝐹 , 𝐻 ⟩ ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) )
259 2 220 211 217 221 223 7 6 227 225 issect2 ⊢ ( 𝜑 → ( ⟨ ◡ 𝐹 , 𝐻 ⟩ ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ⟨ 𝐹 , 𝐺 ⟩ ↔ ( ⟨ 𝐹 , 𝐺 ⟩ ( ⟨ 𝑌 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ⟨ ◡ 𝐹 , 𝐻 ⟩ ) = ( ( Id ‘ 𝐶 ) ‘ 𝑌 ) ) )
260 258 259 mpbird ⊢ ( 𝜑 → ⟨ ◡ 𝐹 , 𝐻 ⟩ ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ⟨ 𝐹 , 𝐺 ⟩ )
261 2 8 223 6 7 221 isinv ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝑋 𝐼 𝑌 ) ⟨ ◡ 𝐹 , 𝐻 ⟩ ↔ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝑋 ( Sect ‘ 𝐶 ) 𝑌 ) ⟨ ◡ 𝐹 , 𝐻 ⟩ ∧ ⟨ ◡ 𝐹 , 𝐻 ⟩ ( 𝑌 ( Sect ‘ 𝐶 ) 𝑋 ) ⟨ 𝐹 , 𝐺 ⟩ ) ) )
262 229 260 261 mpbir2and ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ( 𝑋 𝐼 𝑌 ) ⟨ ◡ 𝐹 , 𝐻 ⟩ )