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 ffvelcdmd ⊒ ( ( πœ‘ ∧ 𝑒 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) β†’ ( 𝐹 β€˜ 𝑒 ) ∈ 𝑆 )
19 simp3 ⊒ ( ( πœ‘ ∧ 𝑒 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) β†’ 𝑣 ∈ 𝑅 )
20 16 19 ffvelcdmd ⊒ ( ( πœ‘ ∧ 𝑒 ∈ 𝑅 ∧ 𝑣 ∈ 𝑅 ) β†’ ( 𝐹 β€˜ 𝑣 ) ∈ 𝑆 )
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 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝑒 ∈ 𝑆 ) β†’ ( β—‘ 𝐹 β€˜ 𝑒 ) ∈ 𝑅 )
77 76 adantrr ⊒ ( ( πœ‘ ∧ ( 𝑒 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ) ) β†’ ( β—‘ 𝐹 β€˜ 𝑒 ) ∈ 𝑅 )
78 70 ffvelcdmda ⊒ ( ( πœ‘ ∧ 𝑣 ∈ 𝑆 ) β†’ ( β—‘ 𝐹 β€˜ 𝑣 ) ∈ 𝑅 )
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 ffvelcdmd ⊒ ( ( πœ‘ ∧ ( 𝑒 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑒 ( Hom β€˜ π‘Œ ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom β€˜ π‘Œ ) 𝑧 ) ) ) β†’ ( β—‘ 𝐹 β€˜ 𝑒 ) ∈ 𝑅 )
134 simp22 ⊒ ( ( πœ‘ ∧ ( 𝑒 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑒 ( Hom β€˜ π‘Œ ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom β€˜ π‘Œ ) 𝑧 ) ) ) β†’ 𝑣 ∈ 𝑆 )
135 131 134 ffvelcdmd ⊒ ( ( πœ‘ ∧ ( 𝑒 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑒 ( Hom β€˜ π‘Œ ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom β€˜ π‘Œ ) 𝑧 ) ) ) β†’ ( β—‘ 𝐹 β€˜ 𝑣 ) ∈ 𝑅 )
136 simp23 ⊒ ( ( πœ‘ ∧ ( 𝑒 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑒 ( Hom β€˜ π‘Œ ) 𝑣 ) ∧ 𝑔 ∈ ( 𝑣 ( Hom β€˜ π‘Œ ) 𝑧 ) ) ) β†’ 𝑧 ∈ 𝑆 )
137 131 136 ffvelcdmd ⊒ ( ( πœ‘ ∧ ( 𝑒 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑒 ( 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 ffvelcdmd ⊒ ( ( πœ‘ ∧ ( 𝑒 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑒 ( 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 ffvelcdmd ⊒ ( ( πœ‘ ∧ ( 𝑒 ∈ 𝑆 ∧ 𝑣 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ) ∧ ( 𝑓 ∈ ( 𝑒 ( 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 ⊒ ( πœ‘ β†’ ⟨ 𝐹 , 𝐺 ⟩ ( 𝑋 𝐼 π‘Œ ) ⟨ β—‘ 𝐹 , 𝐻 ⟩ )