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 ‘ 𝐸 ) ( 𝐹 ‘ 𝑍 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐻 ) ) )