This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funcsetcestrclem9

Description: Lemma 9 for funcsetcestrc . (Contributed by AV, 28-Mar-2020)

Ref Expression
Hypotheses funcsetcestrc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
funcsetcestrc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
funcsetcestrc.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
Assertion funcsetcestrclem9 ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ∧ ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑆 ) 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑆 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 funcsetcestrc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
2 funcsetcestrc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
3 funcsetcestrc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐶 ↦ { ⟨ ( Base ‘ ndx ) , 𝑥 ⟩ } ) )
4 funcsetcestrc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
5 funcsetcestrc.o ⊢ ( 𝜑 → ω ∈ 𝑈 )
6 funcsetcestrc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐶 , 𝑦 ∈ 𝐶 ↦ ( I ↾ ( 𝑦 ↑m 𝑥 ) ) ) )
7 funcsetcestrc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
8 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → 𝑈 ∈ WUni )
9 eqid ⊢ ( Hom ‘ 𝑆 ) = ( Hom ‘ 𝑆 )
10 1 4 setcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝑆 ) )
11 2 10 eqtr4id ⊢ ( 𝜑 → 𝐶 = 𝑈 )
12 11 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐶 ↔ 𝑋 ∈ 𝑈 ) )
13 12 biimpcd ⊢ ( 𝑋 ∈ 𝐶 → ( 𝜑 → 𝑋 ∈ 𝑈 ) )
14 13 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) → ( 𝜑 → 𝑋 ∈ 𝑈 ) )
15 14 impcom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → 𝑋 ∈ 𝑈 )
16 11 eleq2d ⊢ ( 𝜑 → ( 𝑌 ∈ 𝐶 ↔ 𝑌 ∈ 𝑈 ) )
17 16 biimpcd ⊢ ( 𝑌 ∈ 𝐶 → ( 𝜑 → 𝑌 ∈ 𝑈 ) )
18 17 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) → ( 𝜑 → 𝑌 ∈ 𝑈 ) )
19 18 impcom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → 𝑌 ∈ 𝑈 )
20 1 8 9 15 19 setchom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) = ( 𝑌 ↑m 𝑋 ) )
21 20 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) ↔ 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ) )
22 11 eleq2d ⊢ ( 𝜑 → ( 𝑍 ∈ 𝐶 ↔ 𝑍 ∈ 𝑈 ) )
23 22 biimpcd ⊢ ( 𝑍 ∈ 𝐶 → ( 𝜑 → 𝑍 ∈ 𝑈 ) )
24 23 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) → ( 𝜑 → 𝑍 ∈ 𝑈 ) )
25 24 impcom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → 𝑍 ∈ 𝑈 )
26 1 8 9 19 25 setchom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝑌 ( Hom ‘ 𝑆 ) 𝑍 ) = ( 𝑍 ↑m 𝑌 ) )
27 26 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑆 ) 𝑍 ) ↔ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) )
28 21 27 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑆 ) 𝑍 ) ) ↔ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) )
29 elmapi ⊢ ( 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) → 𝐾 : 𝑌 ⟶ 𝑍 )
30 elmapi ⊢ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) → 𝐻 : 𝑋 ⟶ 𝑌 )
31 fco ⊢ ( ( 𝐾 : 𝑌 ⟶ 𝑍 ∧ 𝐻 : 𝑋 ⟶ 𝑌 ) → ( 𝐾 ∘ 𝐻 ) : 𝑋 ⟶ 𝑍 )
32 29 30 31 syl2anr ⊢ ( ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) → ( 𝐾 ∘ 𝐻 ) : 𝑋 ⟶ 𝑍 )
33 32 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( 𝐾 ∘ 𝐻 ) : 𝑋 ⟶ 𝑍 )
34 elmapg ⊢ ( ( 𝑍 ∈ 𝐶 ∧ 𝑋 ∈ 𝐶 ) → ( ( 𝐾 ∘ 𝐻 ) ∈ ( 𝑍 ↑m 𝑋 ) ↔ ( 𝐾 ∘ 𝐻 ) : 𝑋 ⟶ 𝑍 ) )
35 34 ancoms ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) → ( ( 𝐾 ∘ 𝐻 ) ∈ ( 𝑍 ↑m 𝑋 ) ↔ ( 𝐾 ∘ 𝐻 ) : 𝑋 ⟶ 𝑍 ) )
36 35 3adant2 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) → ( ( 𝐾 ∘ 𝐻 ) ∈ ( 𝑍 ↑m 𝑋 ) ↔ ( 𝐾 ∘ 𝐻 ) : 𝑋 ⟶ 𝑍 ) )
37 36 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( 𝐾 ∘ 𝐻 ) ∈ ( 𝑍 ↑m 𝑋 ) ↔ ( 𝐾 ∘ 𝐻 ) : 𝑋 ⟶ 𝑍 ) )
38 33 37 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( 𝐾 ∘ 𝐻 ) ∈ ( 𝑍 ↑m 𝑋 ) )
39 fvresi ⊢ ( ( 𝐾 ∘ 𝐻 ) ∈ ( 𝑍 ↑m 𝑋 ) → ( ( I ↾ ( 𝑍 ↑m 𝑋 ) ) ‘ ( 𝐾 ∘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
40 38 39 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( I ↾ ( 𝑍 ↑m 𝑋 ) ) ‘ ( 𝐾 ∘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
41 1 2 3 4 5 6 funcsetcestrclem5 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝑋 𝐺 𝑍 ) = ( I ↾ ( 𝑍 ↑m 𝑋 ) ) )
42 41 3adantr2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝑋 𝐺 𝑍 ) = ( I ↾ ( 𝑍 ↑m 𝑋 ) ) )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( 𝑋 𝐺 𝑍 ) = ( I ↾ ( 𝑍 ↑m 𝑋 ) ) )
44 8 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → 𝑈 ∈ WUni )
45 eqid ⊢ ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
46 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → 𝑋 ∈ 𝑈 )
47 19 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → 𝑌 ∈ 𝑈 )
48 25 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → 𝑍 ∈ 𝑈 )
49 30 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → 𝐻 : 𝑋 ⟶ 𝑌 )
50 29 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → 𝐾 : 𝑌 ⟶ 𝑍 )
51 1 44 45 46 47 48 49 50 setcco ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑆 ) 𝑍 ) 𝐻 ) = ( 𝐾 ∘ 𝐻 ) )
52 43 51 fveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑆 ) 𝑍 ) 𝐻 ) ) = ( ( I ↾ ( 𝑍 ↑m 𝑋 ) ) ‘ ( 𝐾 ∘ 𝐻 ) ) )
53 eqid ⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
54 1 2 3 4 5 funcsetcestrclem2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
55 54 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
56 55 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
57 1 2 3 4 5 funcsetcestrclem2 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
58 57 3ad2antr2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
59 58 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
60 1 2 3 4 5 funcsetcestrclem2 ⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
61 60 3ad2antr3 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
62 61 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
63 eqid ⊢ ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) = ( Base ‘ ( 𝐹 ‘ 𝑋 ) )
64 eqid ⊢ ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) = ( Base ‘ ( 𝐹 ‘ 𝑌 ) )
65 eqid ⊢ ( Base ‘ ( 𝐹 ‘ 𝑍 ) ) = ( Base ‘ ( 𝐹 ‘ 𝑍 ) )
66 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → 𝜑 )
67 3simpa ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) → ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) )
68 67 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) )
69 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) )
70 1 2 3 4 5 6 funcsetcestrclem6 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ) ∧ 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) = 𝐻 )
71 66 68 69 70 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) = 𝐻 )
72 1 2 3 funcsetcestrclem1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑋 ) = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } )
73 72 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑋 ) = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } )
74 73 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) )
75 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ }
76 75 1strbas ⊢ ( 𝑋 ∈ 𝐶 → 𝑋 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) )
77 76 eqcomd ⊢ ( 𝑋 ∈ 𝐶 → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) = 𝑋 )
78 77 3ad2ant1 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) = 𝑋 )
79 78 adantl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ } ) = 𝑋 )
80 74 79 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝑋 )
81 80 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) = 𝑋 )
82 1 2 3 funcsetcestrclem1 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑌 ) = { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } )
83 82 3ad2antr2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑌 ) = { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } )
84 83 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } ) )
85 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ }
86 85 1strbas ⊢ ( 𝑌 ∈ 𝐶 → 𝑌 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } ) )
87 86 eqcomd ⊢ ( 𝑌 ∈ 𝐶 → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } ) = 𝑌 )
88 87 3ad2ant2 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } ) = 𝑌 )
89 88 adantl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑌 ⟩ } ) = 𝑌 )
90 84 89 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝑌 )
91 90 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) = 𝑌 )
92 71 81 91 feq123d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) : ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) ⟶ ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ↔ 𝐻 : 𝑋 ⟶ 𝑌 ) )
93 49 92 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) : ( Base ‘ ( 𝐹 ‘ 𝑋 ) ) ⟶ ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) )
94 3simpc ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) → ( 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) )
95 94 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) )
96 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) )
97 1 2 3 4 5 6 funcsetcestrclem6 ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) = 𝐾 )
98 66 95 96 97 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) = 𝐾 )
99 1 2 3 funcsetcestrclem1 ⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝐶 ) → ( 𝐹 ‘ 𝑍 ) = { ⟨ ( Base ‘ ndx ) , 𝑍 ⟩ } )
100 99 3ad2antr3 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝐹 ‘ 𝑍 ) = { ⟨ ( Base ‘ ndx ) , 𝑍 ⟩ } )
101 100 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑍 ) ) = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑍 ⟩ } ) )
102 eqid ⊢ { ⟨ ( Base ‘ ndx ) , 𝑍 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑍 ⟩ }
103 102 1strbas ⊢ ( 𝑍 ∈ 𝐶 → 𝑍 = ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑍 ⟩ } ) )
104 103 eqcomd ⊢ ( 𝑍 ∈ 𝐶 → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑍 ⟩ } ) = 𝑍 )
105 104 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑍 ⟩ } ) = 𝑍 )
106 105 adantl ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( Base ‘ { ⟨ ( Base ‘ ndx ) , 𝑍 ⟩ } ) = 𝑍 )
107 101 106 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( Base ‘ ( 𝐹 ‘ 𝑍 ) ) = 𝑍 )
108 107 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( Base ‘ ( 𝐹 ‘ 𝑍 ) ) = 𝑍 )
109 98 91 108 feq123d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) : ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ⟶ ( Base ‘ ( 𝐹 ‘ 𝑍 ) ) ↔ 𝐾 : 𝑌 ⟶ 𝑍 ) )
110 50 109 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) : ( Base ‘ ( 𝐹 ‘ 𝑌 ) ) ⟶ ( Base ‘ ( 𝐹 ‘ 𝑍 ) ) )
111 7 44 53 56 59 62 63 64 65 93 110 estrcco ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ∘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )
112 98 71 coeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ∘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
113 111 112 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
114 40 52 113 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) ∧ ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑆 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )
115 114 ex ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( ( 𝐻 ∈ ( 𝑌 ↑m 𝑋 ) ∧ 𝐾 ∈ ( 𝑍 ↑m 𝑌 ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑆 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) )
116 28 115 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ) → ( ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑆 ) 𝑍 ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑆 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) )
117 116 3impia ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶 ∧ 𝑍 ∈ 𝐶 ) ∧ ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝑆 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝑆 ) 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝑆 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )