funcestrcsetclem8

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

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		f1oi	$⊢ ({I ↾}_{({Base}_{Y}^{{Base}_{X}})}) : {Base}_{Y}^{{Base}_{X}} \underset{1-1 onto}{⟶} {Base}_{Y}^{{Base}_{X}}$
9		f1of	$⊢ ({I ↾}_{({Base}_{Y}^{{Base}_{X}})}) : {Base}_{Y}^{{Base}_{X}} \underset{1-1 onto}{⟶} {Base}_{Y}^{{Base}_{X}} \to ({I ↾}_{({Base}_{Y}^{{Base}_{X}})}) : {Base}_{Y}^{{Base}_{X}} ⟶ {Base}_{Y}^{{Base}_{X}}$
10	8 9	mp1i	$⊢ (φ \land (X \in B \land Y \in B)) \to ({I ↾}_{({Base}_{Y}^{{Base}_{X}})}) : {Base}_{Y}^{{Base}_{X}} ⟶ {Base}_{Y}^{{Base}_{X}}$
11		elmapi	$⊢ f \in ({Base}_{Y}^{{Base}_{X}}) \to f : {Base}_{X} ⟶ {Base}_{Y}$
12		fvex	$⊢ {Base}_{Y} \in V$
13		fvex	$⊢ {Base}_{X} \in V$
14	12 13	pm3.2i	$⊢ ({Base}_{Y} \in V \land {Base}_{X} \in V)$
15		elmapg	$⊢ ({Base}_{Y} \in V \land {Base}_{X} \in V) \to (f \in ({Base}_{Y}^{{Base}_{X}}) \leftrightarrow f : {Base}_{X} ⟶ {Base}_{Y})$
16	15	bicomd	$⊢ ({Base}_{Y} \in V \land {Base}_{X} \in V) \to (f : {Base}_{X} ⟶ {Base}_{Y} \leftrightarrow f \in ({Base}_{Y}^{{Base}_{X}}))$
17	14 16	mp1i	$⊢ (φ \land (X \in B \land Y \in B)) \to (f : {Base}_{X} ⟶ {Base}_{Y} \leftrightarrow f \in ({Base}_{Y}^{{Base}_{X}}))$
18	17	biimpa	$⊢ ((φ \land (X \in B \land Y \in B)) \land f : {Base}_{X} ⟶ {Base}_{Y}) \to f \in ({Base}_{Y}^{{Base}_{X}})$
19	1 2 3 4 5 6	funcestrcsetclem1	$⊢ (φ \land Y \in B) \to F (Y) = {Base}_{Y}$
20	19	adantrl	$⊢ (φ \land (X \in B \land Y \in B)) \to F (Y) = {Base}_{Y}$
21	1 2 3 4 5 6	funcestrcsetclem1	$⊢ (φ \land X \in B) \to F (X) = {Base}_{X}$
22	21	adantrr	$⊢ (φ \land (X \in B \land Y \in B)) \to F (X) = {Base}_{X}$
23	20 22	oveq12d	$⊢ (φ \land (X \in B \land Y \in B)) \to {F (Y)}^{F (X)} = {Base}_{Y}^{{Base}_{X}}$
24	23	adantr	$⊢ ((φ \land (X \in B \land Y \in B)) \land f : {Base}_{X} ⟶ {Base}_{Y}) \to {F (Y)}^{F (X)} = {Base}_{Y}^{{Base}_{X}}$
25	18 24	eleqtrrd	$⊢ ((φ \land (X \in B \land Y \in B)) \land f : {Base}_{X} ⟶ {Base}_{Y}) \to f \in ({F (Y)}^{F (X)})$
26	25	ex	$⊢ (φ \land (X \in B \land Y \in B)) \to (f : {Base}_{X} ⟶ {Base}_{Y} \to f \in ({F (Y)}^{F (X)}))$
27	11 26	syl5	$⊢ (φ \land (X \in B \land Y \in B)) \to (f \in ({Base}_{Y}^{{Base}_{X}}) \to f \in ({F (Y)}^{F (X)}))$
28	27	ssrdv	$⊢ (φ \land (X \in B \land Y \in B)) \to {Base}_{Y}^{{Base}_{X}} \subseteq {F (Y)}^{F (X)}$
29	10 28	fssd	$⊢ (φ \land (X \in B \land Y \in B)) \to ({I ↾}_{({Base}_{Y}^{{Base}_{X}})}) : {Base}_{Y}^{{Base}_{X}} ⟶ {F (Y)}^{F (X)}$
30		eqid	$⊢ {Base}_{X} = {Base}_{X}$
31		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
32	1 2 3 4 5 6 7 30 31	funcestrcsetclem5	$⊢ (φ \land (X \in B \land Y \in B)) \to X G Y = {I ↾}_{({Base}_{Y}^{{Base}_{X}})}$
33	5	adantr	$⊢ (φ \land (X \in B \land Y \in B)) \to U \in WUni$
34		eqid	$⊢ Hom (E) = Hom (E)$
35	1 5	estrcbas	$⊢ φ \to U = {Base}_{E}$
36	3 35	eqtr4id	$⊢ φ \to B = U$
37	36	eleq2d	$⊢ φ \to (X \in B \leftrightarrow X \in U)$
38	37	biimpcd	$⊢ X \in B \to (φ \to X \in U)$
39	38	adantr	$⊢ (X \in B \land Y \in B) \to (φ \to X \in U)$
40	39	impcom	$⊢ (φ \land (X \in B \land Y \in B)) \to X \in U$
41	36	eleq2d	$⊢ φ \to (Y \in B \leftrightarrow Y \in U)$
42	41	biimpd	$⊢ φ \to (Y \in B \to Y \in U)$
43	42	adantld	$⊢ φ \to ((X \in B \land Y \in B) \to Y \in U)$
44	43	imp	$⊢ (φ \land (X \in B \land Y \in B)) \to Y \in U$
45	1 33 34 40 44 30 31	estrchom	$⊢ (φ \land (X \in B \land Y \in B)) \to X Hom (E) Y = {Base}_{Y}^{{Base}_{X}}$
46		eqid	$⊢ Hom (S) = Hom (S)$
47	1 2 3 4 5 6	funcestrcsetclem2	$⊢ (φ \land X \in B) \to F (X) \in U$
48	47	adantrr	$⊢ (φ \land (X \in B \land Y \in B)) \to F (X) \in U$
49	1 2 3 4 5 6	funcestrcsetclem2	$⊢ (φ \land Y \in B) \to F (Y) \in U$
50	49	adantrl	$⊢ (φ \land (X \in B \land Y \in B)) \to F (Y) \in U$
51	2 33 46 48 50	setchom	$⊢ (φ \land (X \in B \land Y \in B)) \to F (X) Hom (S) F (Y) = {F (Y)}^{F (X)}$
52	32 45 51	feq123d	$⊢ (φ \land (X \in B \land Y \in B)) \to ((X G Y) : X Hom (E) Y ⟶ F (X) Hom (S) F (Y) \leftrightarrow ({I ↾}_{({Base}_{Y}^{{Base}_{X}})}) : {Base}_{Y}^{{Base}_{X}} ⟶ {F (Y)}^{F (X)})$
53	29 52	mpbird	$⊢ (φ \land (X \in B \land Y \in B)) \to (X G Y) : X Hom (E) Y ⟶ F (X) Hom (S) F (Y)$

Metamath Proof Explorer

Theorem funcestrcsetclem8

Proof