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

Metamath Proof Explorer

Theorem funcestrcsetclem9

Description: Lemma 9 for funcestrcsetc . (Contributed by AV, 23-Mar-2020)

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

Proof

Step Hyp Ref Expression
1 funcestrcsetc.e ⊢ 𝐸 = ( ExtStrCat ‘ 𝑈 )
2 funcestrcsetc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
3 funcestrcsetc.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
4 funcestrcsetc.c ⊢ 𝐶 = ( Base ‘ 𝑆 )
5 funcestrcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
6 funcestrcsetc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
7 funcestrcsetc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) )
8 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑈 ∈ WUni )
9 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
10 1 5 estrcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ 𝐸 ) )
11 3 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 eqid ⊢ ( Base ‘ 𝑋 ) = ( Base ‘ 𝑋 )
21 eqid ⊢ ( Base ‘ 𝑌 ) = ( Base ‘ 𝑌 )
22 1 8 9 15 19 20 21 estrchom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 ( Hom ‘ 𝐸 ) 𝑌 ) = ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
23 22 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐸 ) 𝑌 ) ↔ 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) )
24 11 eleq2d ⊢ ( 𝜑 → ( 𝑍 ∈ 𝐵 ↔ 𝑍 ∈ 𝑈 ) )
25 24 biimpcd ⊢ ( 𝑍 ∈ 𝐵 → ( 𝜑 → 𝑍 ∈ 𝑈 ) )
26 25 3ad2ant3 ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝜑 → 𝑍 ∈ 𝑈 ) )
27 26 impcom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → 𝑍 ∈ 𝑈 )
28 eqid ⊢ ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
29 1 8 9 19 27 21 28 estrchom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑌 ( Hom ‘ 𝐸 ) 𝑍 ) = ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) )
30 29 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝐸 ) 𝑍 ) ↔ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) )
31 23 30 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐸 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝐸 ) 𝑍 ) ) ↔ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) )
32 elmapi ⊢ ( 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) → 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) )
33 elmapi ⊢ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) → 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
34 fco ⊢ ( ( 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) ∧ 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) → ( 𝐾 ∘ 𝐻 ) : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑍 ) )
35 32 33 34 syl2an ⊢ ( ( 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ∧ 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) → ( 𝐾 ∘ 𝐻 ) : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑍 ) )
36 fvex ⊢ ( Base ‘ 𝑍 ) ∈ V
37 fvex ⊢ ( Base ‘ 𝑋 ) ∈ V
38 36 37 elmap ⊢ ( ( 𝐾 ∘ 𝐻 ) ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑋 ) ) ↔ ( 𝐾 ∘ 𝐻 ) : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑍 ) )
39 35 38 sylibr ⊢ ( ( 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ∧ 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) → ( 𝐾 ∘ 𝐻 ) ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑋 ) ) )
40 39 ancoms ⊢ ( ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) → ( 𝐾 ∘ 𝐻 ) ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑋 ) ) )
41 40 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( 𝐾 ∘ 𝐻 ) ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑋 ) ) )
42 fvresi ⊢ ( ( 𝐾 ∘ 𝐻 ) ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑋 ) ) → ( ( I ↾ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑋 ) ) ) ‘ ( 𝐾 ∘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
43 41 42 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( I ↾ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑋 ) ) ) ‘ ( 𝐾 ∘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
44 1 2 3 4 5 6 7 20 28 funcestrcsetclem5 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐺 𝑍 ) = ( I ↾ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑋 ) ) ) )
45 44 3adantr2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝑋 𝐺 𝑍 ) = ( I ↾ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑋 ) ) ) )
46 45 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( 𝑋 𝐺 𝑍 ) = ( I ↾ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑋 ) ) ) )
47 8 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → 𝑈 ∈ WUni )
48 eqid ⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
49 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → 𝑋 ∈ 𝑈 )
50 19 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → 𝑌 ∈ 𝑈 )
51 27 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → 𝑍 ∈ 𝑈 )
52 33 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) )
53 32 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) )
54 1 47 48 49 50 51 20 21 28 52 53 estrcco ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐸 ) 𝑍 ) 𝐻 ) = ( 𝐾 ∘ 𝐻 ) )
55 46 54 fveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐸 ) 𝑍 ) 𝐻 ) ) = ( ( I ↾ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑋 ) ) ) ‘ ( 𝐾 ∘ 𝐻 ) ) )
56 eqid ⊢ ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
57 1 2 3 4 5 6 funcestrcsetclem2 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
58 57 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
59 58 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ 𝑋 ) ∈ 𝑈 )
60 1 2 3 4 5 6 funcestrcsetclem2 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
61 60 3ad2antr2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
62 61 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ 𝑌 ) ∈ 𝑈 )
63 1 2 3 4 5 6 funcestrcsetclem2 ⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
64 63 3ad2antr3 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
65 64 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( 𝐹 ‘ 𝑍 ) ∈ 𝑈 )
66 1 2 3 4 5 6 funcestrcsetclem1 ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) = ( Base ‘ 𝑋 ) )
67 66 3ad2antr1 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑋 ) = ( Base ‘ 𝑋 ) )
68 1 2 3 4 5 6 funcestrcsetclem1 ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
69 68 3ad2antr2 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑌 ) = ( Base ‘ 𝑌 ) )
70 67 69 feq23d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ↔ 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) )
71 70 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ↔ 𝐻 : ( Base ‘ 𝑋 ) ⟶ ( Base ‘ 𝑌 ) ) )
72 52 71 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) )
73 simpll ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → 𝜑 )
74 3simpa ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
75 74 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) )
76 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) )
77 1 2 3 4 5 6 7 20 21 funcestrcsetclem6 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) = 𝐻 )
78 73 75 76 77 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) = 𝐻 )
79 78 feq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ↔ 𝐻 : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) ) )
80 72 79 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) : ( 𝐹 ‘ 𝑋 ) ⟶ ( 𝐹 ‘ 𝑌 ) )
81 1 2 3 4 5 6 funcestrcsetclem1 ⊢ ( ( 𝜑 ∧ 𝑍 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑍 ) = ( Base ‘ 𝑍 ) )
82 81 3ad2antr3 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑍 ) = ( Base ‘ 𝑍 ) )
83 69 82 feq23d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ↔ 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) ) )
84 83 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ↔ 𝐾 : ( Base ‘ 𝑌 ) ⟶ ( Base ‘ 𝑍 ) ) )
85 53 84 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) )
86 3simpc ⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) → ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) )
87 86 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) )
88 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) )
89 1 2 3 4 5 6 7 21 28 funcestrcsetclem6 ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) = 𝐾 )
90 73 87 88 89 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) = 𝐾 )
91 90 feq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ↔ 𝐾 : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) ) )
92 85 91 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) : ( 𝐹 ‘ 𝑌 ) ⟶ ( 𝐹 ‘ 𝑍 ) )
93 2 47 56 59 62 65 80 92 setcco ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ∘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )
94 90 78 coeq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ∘ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
95 93 94 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) = ( 𝐾 ∘ 𝐻 ) )
96 43 55 95 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) ∧ ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐸 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )
97 96 ex ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝐻 ∈ ( ( Base ‘ 𝑌 ) ↑m ( Base ‘ 𝑋 ) ) ∧ 𝐾 ∈ ( ( Base ‘ 𝑍 ) ↑m ( Base ‘ 𝑌 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐸 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) )
98 31 97 sylbid ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ) → ( ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐸 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝐸 ) 𝑍 ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐸 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) ) )
99 98 3impia ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝑋 ( Hom ‘ 𝐸 ) 𝑌 ) ∧ 𝐾 ∈ ( 𝑌 ( Hom ‘ 𝐸 ) 𝑍 ) ) ) → ( ( 𝑋 𝐺 𝑍 ) ‘ ( 𝐾 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐸 ) 𝑍 ) 𝐻 ) ) = ( ( ( 𝑌 𝐺 𝑍 ) ‘ 𝐾 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )