funcestrcsetclem9

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

Proof

Step	Hyp	Ref	Expression
1		funcestrcsetc.e	$⊢ E = ExtStrCat (U)$
2		funcestrcsetc.s	$⊢ S = SetCat (U)$
3		funcestrcsetc.b	$⊢ B = {Base}_{E}$
4		funcestrcsetc.c	$⊢ C = {Base}_{S}$
5		funcestrcsetc.u	$⊢ φ \to U \in WUni$
6		funcestrcsetc.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
7		funcestrcsetc.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{({Base}_{y}^{{Base}_{x}})})$
8	5	adantr	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to U \in WUni$
9		eqid	$⊢ Hom (E) = Hom (E)$
10	1 5	estrcbas	$⊢ φ \to U = {Base}_{E}$
11	10 3	syl6reqr	$⊢ φ \to B = U$
12	11	eleq2d	$⊢ φ \to (X \in B \leftrightarrow X \in U)$
13	12	biimpcd	$⊢ X \in B \to (φ \to X \in U)$
14	13	3ad2ant1	$⊢ (X \in B \land Y \in B \land Z \in B) \to (φ \to X \in U)$
15	14	impcom	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to X \in U$
16	11	eleq2d	$⊢ φ \to (Y \in B \leftrightarrow Y \in U)$
17	16	biimpcd	$⊢ Y \in B \to (φ \to Y \in U)$
18	17	3ad2ant2	$⊢ (X \in B \land Y \in B \land Z \in B) \to (φ \to Y \in U)$
19	18	impcom	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to Y \in U$
20		eqid	$⊢ {Base}_{X} = {Base}_{X}$
21		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
22	1 8 9 15 19 20 21	estrchom	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to X Hom (E) Y = {Base}_{Y}^{{Base}_{X}}$
23	22	eleq2d	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to (H \in (X Hom (E) Y) \leftrightarrow H \in ({Base}_{Y}^{{Base}_{X}}))$
24	11	eleq2d	$⊢ φ \to (Z \in B \leftrightarrow Z \in U)$
25	24	biimpcd	$⊢ Z \in B \to (φ \to Z \in U)$
26	25	3ad2ant3	$⊢ (X \in B \land Y \in B \land Z \in B) \to (φ \to Z \in U)$
27	26	impcom	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to Z \in U$
28		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
29	1 8 9 19 27 21 28	estrchom	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to Y Hom (E) Z = {Base}_{Z}^{{Base}_{Y}}$
30	29	eleq2d	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to (K \in (Y Hom (E) Z) \leftrightarrow K \in ({Base}_{Z}^{{Base}_{Y}}))$
31	23 30	anbi12d	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to ((H \in (X Hom (E) Y) \land K \in (Y Hom (E) Z)) \leftrightarrow (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}})))$
32		elmapi	$⊢ K \in ({Base}_{Z}^{{Base}_{Y}}) \to K : {Base}_{Y} ⟶ {Base}_{Z}$
33		elmapi	$⊢ H \in ({Base}_{Y}^{{Base}_{X}}) \to H : {Base}_{X} ⟶ {Base}_{Y}$
34		fco	$⊢ (K : {Base}_{Y} ⟶ {Base}_{Z} \land H : {Base}_{X} ⟶ {Base}_{Y}) \to (K \circ H) : {Base}_{X} ⟶ {Base}_{Z}$
35	32 33 34	syl2an	$⊢ (K \in ({Base}_{Z}^{{Base}_{Y}}) \land H \in ({Base}_{Y}^{{Base}_{X}})) \to (K \circ H) : {Base}_{X} ⟶ {Base}_{Z}$
36		fvex	$⊢ {Base}_{Z} \in V$
37		fvex	$⊢ {Base}_{X} \in V$
38	36 37	elmap	$⊢ K \circ H \in ({Base}_{Z}^{{Base}_{X}}) \leftrightarrow (K \circ H) : {Base}_{X} ⟶ {Base}_{Z}$
39	35 38	sylibr	$⊢ (K \in ({Base}_{Z}^{{Base}_{Y}}) \land H \in ({Base}_{Y}^{{Base}_{X}})) \to K \circ H \in ({Base}_{Z}^{{Base}_{X}})$
40	39	ancoms	$⊢ (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}})) \to K \circ H \in ({Base}_{Z}^{{Base}_{X}})$
41	40	adantl	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to K \circ H \in ({Base}_{Z}^{{Base}_{X}})$
42		fvresi	$⊢ K \circ H \in ({Base}_{Z}^{{Base}_{X}}) \to ({I ↾}_{({Base}_{Z}^{{Base}_{X}})}) (K \circ H) = K \circ H$
43	41 42	syl	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to ({I ↾}_{({Base}_{Z}^{{Base}_{X}})}) (K \circ H) = K \circ H$
44	1 2 3 4 5 6 7 20 28	funcestrcsetclem5	$⊢ (φ \land (X \in B \land Z \in B)) \to X G Z = {I ↾}_{({Base}_{Z}^{{Base}_{X}})}$
45	44	3adantr2	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to X G Z = {I ↾}_{({Base}_{Z}^{{Base}_{X}})}$
46	45	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to X G Z = {I ↾}_{({Base}_{Z}^{{Base}_{X}})}$
47	8	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to U \in WUni$
48		eqid	$⊢ comp (E) = comp (E)$
49	15	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to X \in U$
50	19	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to Y \in U$
51	27	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to Z \in U$
52	33	ad2antrl	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to H : {Base}_{X} ⟶ {Base}_{Y}$
53	32	ad2antll	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to K : {Base}_{Y} ⟶ {Base}_{Z}$
54	1 47 48 49 50 51 20 21 28 52 53	estrcco	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to K (⟨X, Y⟩ comp (E) Z) H = K \circ H$
55	46 54	fveq12d	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (X G Z) (K (⟨X, Y⟩ comp (E) Z) H) = ({I ↾}_{({Base}_{Z}^{{Base}_{X}})}) (K \circ H)$
56		eqid	$⊢ comp (S) = comp (S)$
57	1 2 3 4 5 6	funcestrcsetclem2	$⊢ (φ \land X \in B) \to F (X) \in U$
58	57	3ad2antr1	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (X) \in U$
59	58	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to F (X) \in U$
60	1 2 3 4 5 6	funcestrcsetclem2	$⊢ (φ \land Y \in B) \to F (Y) \in U$
61	60	3ad2antr2	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Y) \in U$
62	61	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to F (Y) \in U$
63	1 2 3 4 5 6	funcestrcsetclem2	$⊢ (φ \land Z \in B) \to F (Z) \in U$
64	63	3ad2antr3	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Z) \in U$
65	64	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to F (Z) \in U$
66	1 2 3 4 5 6	funcestrcsetclem1	$⊢ (φ \land X \in B) \to F (X) = {Base}_{X}$
67	66	3ad2antr1	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (X) = {Base}_{X}$
68	1 2 3 4 5 6	funcestrcsetclem1	$⊢ (φ \land Y \in B) \to F (Y) = {Base}_{Y}$
69	68	3ad2antr2	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Y) = {Base}_{Y}$
70	67 69	feq23d	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to (H : F (X) ⟶ F (Y) \leftrightarrow H : {Base}_{X} ⟶ {Base}_{Y})$
71	70	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (H : F (X) ⟶ F (Y) \leftrightarrow H : {Base}_{X} ⟶ {Base}_{Y})$
72	52 71	mpbird	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to H : F (X) ⟶ F (Y)$
73		simpll	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to φ$
74		3simpa	$⊢ (X \in B \land Y \in B \land Z \in B) \to (X \in B \land Y \in B)$
75	74	ad2antlr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (X \in B \land Y \in B)$
76		simprl	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to H \in ({Base}_{Y}^{{Base}_{X}})$
77	1 2 3 4 5 6 7 20 21	funcestrcsetclem6	$⊢ (φ \land (X \in B \land Y \in B) \land H \in ({Base}_{Y}^{{Base}_{X}})) \to (X G Y) (H) = H$
78	73 75 76 77	syl3anc	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (X G Y) (H) = H$
79	78	feq1d	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to ((X G Y) (H) : F (X) ⟶ F (Y) \leftrightarrow H : F (X) ⟶ F (Y))$
80	72 79	mpbird	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (X G Y) (H) : F (X) ⟶ F (Y)$
81	1 2 3 4 5 6	funcestrcsetclem1	$⊢ (φ \land Z \in B) \to F (Z) = {Base}_{Z}$
82	81	3ad2antr3	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Z) = {Base}_{Z}$
83	69 82	feq23d	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to (K : F (Y) ⟶ F (Z) \leftrightarrow K : {Base}_{Y} ⟶ {Base}_{Z})$
84	83	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (K : F (Y) ⟶ F (Z) \leftrightarrow K : {Base}_{Y} ⟶ {Base}_{Z})$
85	53 84	mpbird	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to K : F (Y) ⟶ F (Z)$
86		3simpc	$⊢ (X \in B \land Y \in B \land Z \in B) \to (Y \in B \land Z \in B)$
87	86	ad2antlr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (Y \in B \land Z \in B)$
88		simprr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to K \in ({Base}_{Z}^{{Base}_{Y}})$
89	1 2 3 4 5 6 7 21 28	funcestrcsetclem6	$⊢ (φ \land (Y \in B \land Z \in B) \land K \in ({Base}_{Z}^{{Base}_{Y}})) \to (Y G Z) (K) = K$
90	73 87 88 89	syl3anc	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (Y G Z) (K) = K$
91	90	feq1d	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to ((Y G Z) (K) : F (Y) ⟶ F (Z) \leftrightarrow K : F (Y) ⟶ F (Z))$
92	85 91	mpbird	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (Y G Z) (K) : F (Y) ⟶ F (Z)$
93	2 47 56 59 62 65 80 92	setcco	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H) = (Y G Z) (K) \circ (X G Y) (H)$
94	90 78	coeq12d	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (Y G Z) (K) \circ (X G Y) (H) = K \circ H$
95	93 94	eqtrd	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H) = K \circ H$
96	43 55 95	3eqtr4d	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}}))) \to (X G Z) (K (⟨X, Y⟩ comp (E) Z) H) = (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H)$
97	96	ex	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to ((H \in ({Base}_{Y}^{{Base}_{X}}) \land K \in ({Base}_{Z}^{{Base}_{Y}})) \to (X G Z) (K (⟨X, Y⟩ comp (E) Z) H) = (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H))$
98	31 97	sylbid	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to ((H \in (X Hom (E) Y) \land K \in (Y Hom (E) Z)) \to (X G Z) (K (⟨X, Y⟩ comp (E) Z) H) = (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H))$
99	98	3impia	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B) \land (H \in (X Hom (E) Y) \land K \in (Y Hom (E) Z))) \to (X G Z) (K (⟨X, Y⟩ comp (E) Z) H) = (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H)$

Metamath Proof Explorer

Theorem funcestrcsetclem9

Proof