funcsetcestrclem9

	Ref	Expression
Hypotheses	funcsetcestrc.s	$⊢ S = SetCat (U)$
	funcsetcestrc.c	$⊢ C = {Base}_{S}$
	funcsetcestrc.f	$⊢ φ \to F = (x \in C ⟼ \{⟨{Base}_{ndx}, x⟩\})$
	funcsetcestrc.u	$⊢ φ \to U \in WUni$
	funcsetcestrc.o	$⊢ φ \to ω \in U$
	funcsetcestrc.g	$⊢ φ \to G = (x \in C, y \in C ⟼ {I ↾}_{(y^{x})})$
	funcsetcestrc.e	$⊢ E = ExtStrCat (U)$
Assertion	funcsetcestrclem9	$⊢ (φ \land (X \in C \land Y \in C \land Z \in C) \land (H \in (X Hom (S) Y) \land K \in (Y Hom (S) Z))) \to (X G Z) (K (⟨X, Y⟩ comp (S) Z) H) = (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (E) F (Z)) (X G Y) (H)$

Proof

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

Metamath Proof Explorer

Theorem funcsetcestrclem9

Proof