funcsetcestrclem8

	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	funcsetcestrclem8	$⊢ (φ \land (X \in C \land Y \in C)) \to (X G Y) : X Hom (S) Y ⟶ F (X) Hom (E) F (Y)$

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		f1oi	$⊢ ({I ↾}_{(Y^{X})}) : Y^{X} \underset{1-1 onto}{⟶} Y^{X}$
9		f1of	$⊢ ({I ↾}_{(Y^{X})}) : Y^{X} \underset{1-1 onto}{⟶} Y^{X} \to ({I ↾}_{(Y^{X})}) : Y^{X} ⟶ Y^{X}$
10	8 9	mp1i	$⊢ (φ \land (X \in C \land Y \in C)) \to ({I ↾}_{(Y^{X})}) : Y^{X} ⟶ Y^{X}$
11		elmapi	$⊢ f \in (Y^{X}) \to f : X ⟶ Y$
12		simpr	$⊢ (φ \land (X \in C \land Y \in C)) \to (X \in C \land Y \in C)$
13	12	ancomd	$⊢ (φ \land (X \in C \land Y \in C)) \to (Y \in C \land X \in C)$
14		elmapg	$⊢ (Y \in C \land X \in C) \to (f \in (Y^{X}) \leftrightarrow f : X ⟶ Y)$
15	13 14	syl	$⊢ (φ \land (X \in C \land Y \in C)) \to (f \in (Y^{X}) \leftrightarrow f : X ⟶ Y)$
16	15	biimpar	$⊢ ((φ \land (X \in C \land Y \in C)) \land f : X ⟶ Y) \to f \in (Y^{X})$
17	1 2 3	funcsetcestrclem1	$⊢ (φ \land Y \in C) \to F (Y) = \{⟨{Base}_{ndx}, Y⟩\}$
18	17	fveq2d	$⊢ (φ \land Y \in C) \to {Base}_{F (Y)} = {Base}_{\{⟨{Base}_{ndx}, Y⟩\}}$
19		eqid	$⊢ \{⟨{Base}_{ndx}, Y⟩\} = \{⟨{Base}_{ndx}, Y⟩\}$
20	19	1strbas	$⊢ Y \in C \to Y = {Base}_{\{⟨{Base}_{ndx}, Y⟩\}}$
21	20	eqcomd	$⊢ Y \in C \to {Base}_{\{⟨{Base}_{ndx}, Y⟩\}} = Y$
22	21	adantl	$⊢ (φ \land Y \in C) \to {Base}_{\{⟨{Base}_{ndx}, Y⟩\}} = Y$
23	18 22	eqtrd	$⊢ (φ \land Y \in C) \to {Base}_{F (Y)} = Y$
24	23	adantrl	$⊢ (φ \land (X \in C \land Y \in C)) \to {Base}_{F (Y)} = Y$
25	1 2 3	funcsetcestrclem1	$⊢ (φ \land X \in C) \to F (X) = \{⟨{Base}_{ndx}, X⟩\}$
26	25	fveq2d	$⊢ (φ \land X \in C) \to {Base}_{F (X)} = {Base}_{\{⟨{Base}_{ndx}, X⟩\}}$
27		eqid	$⊢ \{⟨{Base}_{ndx}, X⟩\} = \{⟨{Base}_{ndx}, X⟩\}$
28	27	1strbas	$⊢ X \in C \to X = {Base}_{\{⟨{Base}_{ndx}, X⟩\}}$
29	28	adantl	$⊢ (φ \land X \in C) \to X = {Base}_{\{⟨{Base}_{ndx}, X⟩\}}$
30	26 29	eqtr4d	$⊢ (φ \land X \in C) \to {Base}_{F (X)} = X$
31	30	adantrr	$⊢ (φ \land (X \in C \land Y \in C)) \to {Base}_{F (X)} = X$
32	24 31	oveq12d	$⊢ (φ \land (X \in C \land Y \in C)) \to {Base}_{F (Y)}^{{Base}_{F (X)}} = Y^{X}$
33	32	adantr	$⊢ ((φ \land (X \in C \land Y \in C)) \land f : X ⟶ Y) \to {Base}_{F (Y)}^{{Base}_{F (X)}} = Y^{X}$
34	16 33	eleqtrrd	$⊢ ((φ \land (X \in C \land Y \in C)) \land f : X ⟶ Y) \to f \in ({Base}_{F (Y)}^{{Base}_{F (X)}})$
35	34	ex	$⊢ (φ \land (X \in C \land Y \in C)) \to (f : X ⟶ Y \to f \in ({Base}_{F (Y)}^{{Base}_{F (X)}}))$
36	11 35	syl5	$⊢ (φ \land (X \in C \land Y \in C)) \to (f \in (Y^{X}) \to f \in ({Base}_{F (Y)}^{{Base}_{F (X)}}))$
37	36	ssrdv	$⊢ (φ \land (X \in C \land Y \in C)) \to Y^{X} \subseteq {Base}_{F (Y)}^{{Base}_{F (X)}}$
38	10 37	fssd	$⊢ (φ \land (X \in C \land Y \in C)) \to ({I ↾}_{(Y^{X})}) : Y^{X} ⟶ {Base}_{F (Y)}^{{Base}_{F (X)}}$
39	1 2 3 4 5 6	funcsetcestrclem5	$⊢ (φ \land (X \in C \land Y \in C)) \to X G Y = {I ↾}_{(Y^{X})}$
40	4	adantr	$⊢ (φ \land (X \in C \land Y \in C)) \to U \in WUni$
41		eqid	$⊢ Hom (S) = Hom (S)$
42	1 4	setcbas	$⊢ φ \to U = {Base}_{S}$
43	2 42	eqtr4id	$⊢ φ \to C = U$
44	43	eleq2d	$⊢ φ \to (X \in C \leftrightarrow X \in U)$
45	44	biimpd	$⊢ φ \to (X \in C \to X \in U)$
46	45	adantrd	$⊢ φ \to ((X \in C \land Y \in C) \to X \in U)$
47	46	imp	$⊢ (φ \land (X \in C \land Y \in C)) \to X \in U$
48	43	eleq2d	$⊢ φ \to (Y \in C \leftrightarrow Y \in U)$
49	48	biimpd	$⊢ φ \to (Y \in C \to Y \in U)$
50	49	adantld	$⊢ φ \to ((X \in C \land Y \in C) \to Y \in U)$
51	50	imp	$⊢ (φ \land (X \in C \land Y \in C)) \to Y \in U$
52	1 40 41 47 51	setchom	$⊢ (φ \land (X \in C \land Y \in C)) \to X Hom (S) Y = Y^{X}$
53		eqid	$⊢ Hom (E) = Hom (E)$
54	1 2 3 4 5	funcsetcestrclem2	$⊢ (φ \land X \in C) \to F (X) \in U$
55	54	adantrr	$⊢ (φ \land (X \in C \land Y \in C)) \to F (X) \in U$
56	1 2 3 4 5	funcsetcestrclem2	$⊢ (φ \land Y \in C) \to F (Y) \in U$
57	56	adantrl	$⊢ (φ \land (X \in C \land Y \in C)) \to F (Y) \in U$
58		eqid	$⊢ {Base}_{F (X)} = {Base}_{F (X)}$
59		eqid	$⊢ {Base}_{F (Y)} = {Base}_{F (Y)}$
60	7 40 53 55 57 58 59	estrchom	$⊢ (φ \land (X \in C \land Y \in C)) \to F (X) Hom (E) F (Y) = {Base}_{F (Y)}^{{Base}_{F (X)}}$
61	39 52 60	feq123d	$⊢ (φ \land (X \in C \land Y \in C)) \to ((X G Y) : X Hom (S) Y ⟶ F (X) Hom (E) F (Y) \leftrightarrow ({I ↾}_{(Y^{X})}) : Y^{X} ⟶ {Base}_{F (Y)}^{{Base}_{F (X)}})$
62	38 61	mpbird	$⊢ (φ \land (X \in C \land Y \in C)) \to (X G Y) : X Hom (S) Y ⟶ F (X) Hom (E) F (Y)$

Metamath Proof Explorer

Theorem funcsetcestrclem8

Proof