Theorem funcestrcsetclem8

Description: Lemma 8 for funcestrcsetc . (Contributed by AV, 15-Feb-2020)

	Ref	Expression
Hypotheses	funcestrcsetc.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
	funcestrcsetc.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
	funcestrcsetc.b	$$⊢B={\mathrm{Base}}_E$$
	funcestrcsetc.c	$$⊢C={\mathrm{Base}}_S$$
	funcestrcsetc.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	funcestrcsetc.f	$$⊢\phi \to F=\left(x\in B⟼{\mathrm{Base}}_x\right)$$
	funcestrcsetc.g	$$⊢\phi \to G=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)$$
Assertion	funcestrcsetclem8	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(XGY\right):X\mathrm{Hom}\left(E\right)Y⟶F\left(X\right)\mathrm{Hom}\left(S\right)F\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		funcestrcsetc.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
2		funcestrcsetc.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
3		funcestrcsetc.b	$$⊢B={\mathrm{Base}}_E$$
4		funcestrcsetc.c	$$⊢C={\mathrm{Base}}_S$$
5		funcestrcsetc.u	$$⊢\phi \to U\in \mathrm{WUni}$$
6		funcestrcsetc.f	$$⊢\phi \to F=\left(x\in B⟼{\mathrm{Base}}_x\right)$$
7		funcestrcsetc.g	$$⊢\phi \to G=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_y}^{{\mathrm{Base}}_x}\right)}\right)$$
8		f1oi	$$⊢\left({\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)}\right):{{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\underset{1-1\; onto}{⟶}{{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}$$
9		f1of	$$⊢\left({\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)}\right):{{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\underset{1-1\; onto}{⟶}{{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\to \left({\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)}\right):{{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}⟶{{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}$$
10	8 9	mp1i	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \left({\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)}\right):{{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}⟶{{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}$$
11		elmapi	$$⊢f\in \left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)\to f:{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y$$
12		fvex	$$⊢{\mathrm{Base}}_Y\in \mathrm{V}$$
13		fvex	$$⊢{\mathrm{Base}}_X\in \mathrm{V}$$
14	12 13	pm3.2i	$$⊢\left({\mathrm{Base}}_Y\in \mathrm{V}\wedge {\mathrm{Base}}_X\in \mathrm{V}\right)$$
15		elmapg	$$⊢\left({\mathrm{Base}}_Y\in \mathrm{V}\wedge {\mathrm{Base}}_X\in \mathrm{V}\right)\to \left(f\in \left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)\leftrightarrow f:{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y\right)$$
16	15	bicomd	$$⊢\left({\mathrm{Base}}_Y\in \mathrm{V}\wedge {\mathrm{Base}}_X\in \mathrm{V}\right)\to \left(f:{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y\leftrightarrow f\in \left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)\right)$$
17	14 16	mp1i	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(f:{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y\leftrightarrow f\in \left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)\right)$$
18	17	biimpa	$$⊢\left(\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\wedge f:{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y\right)\to f\in \left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)$$
19	1 2 3 4 5 6	funcestrcsetclem1	$$⊢\left(\phi \wedge Y\in B\right)\to F\left(Y\right)={\mathrm{Base}}_Y$$
20	19	adantrl	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to F\left(Y\right)={\mathrm{Base}}_Y$$
21	1 2 3 4 5 6	funcestrcsetclem1	$$⊢\left(\phi \wedge X\in B\right)\to F\left(X\right)={\mathrm{Base}}_X$$
22	21	adantrr	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to F\left(X\right)={\mathrm{Base}}_X$$
23	20 22	oveq12d	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to {F\left(Y\right)}^{F\left(X\right)}={{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}$$
24	23	adantr	$$⊢\left(\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\wedge f:{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y\right)\to {F\left(Y\right)}^{F\left(X\right)}={{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}$$
25	18 24	eleqtrrd	$$⊢\left(\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\wedge f:{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y\right)\to f\in \left({F\left(Y\right)}^{F\left(X\right)}\right)$$
26	25	ex	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(f:{\mathrm{Base}}_X⟶{\mathrm{Base}}_Y\to f\in \left({F\left(Y\right)}^{F\left(X\right)}\right)\right)$$
27	11 26	syl5	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(f\in \left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)\to f\in \left({F\left(Y\right)}^{F\left(X\right)}\right)\right)$$
28	27	ssrdv	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to {{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\subseteq {F\left(Y\right)}^{F\left(X\right)}$$
29	10 28	fssd	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \left({\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)}\right):{{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}⟶{F\left(Y\right)}^{F\left(X\right)}$$
30		eqid	$$⊢{\mathrm{Base}}_X={\mathrm{Base}}_X$$
31		eqid	$$⊢{\mathrm{Base}}_Y={\mathrm{Base}}_Y$$
32	1 2 3 4 5 6 7 30 31	funcestrcsetclem5	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to XGY={\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)}$$
33	5	adantr	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to U\in \mathrm{WUni}$$
34		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
35	1 5	estrcbas	$$⊢\phi \to U={\mathrm{Base}}_E$$
36	35 3	syl6reqr	$$⊢\phi \to B=U$$
37	36	eleq2d	$$⊢\phi \to \left(X\in B\leftrightarrow X\in U\right)$$
38	37	biimpcd	$$⊢X\in B\to \left(\phi \to X\in U\right)$$
39	38	adantr	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(\phi \to X\in U\right)$$
40	39	impcom	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X\in U$$
41	36	eleq2d	$$⊢\phi \to \left(Y\in B\leftrightarrow Y\in U\right)$$
42	41	biimpd	$$⊢\phi \to \left(Y\in B\to Y\in U\right)$$
43	42	adantld	$$⊢\phi \to \left(\left(X\in B\wedge Y\in B\right)\to Y\in U\right)$$
44	43	imp	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to Y\in U$$
45	1 33 34 40 44 30 31	estrchom	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to X\mathrm{Hom}\left(E\right)Y={{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}$$
46		eqid	$$⊢\mathrm{Hom}\left(S\right)=\mathrm{Hom}\left(S\right)$$
47	1 2 3 4 5 6	funcestrcsetclem2	$$⊢\left(\phi \wedge X\in B\right)\to F\left(X\right)\in U$$
48	47	adantrr	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to F\left(X\right)\in U$$
49	1 2 3 4 5 6	funcestrcsetclem2	$$⊢\left(\phi \wedge Y\in B\right)\to F\left(Y\right)\in U$$
50	49	adantrl	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to F\left(Y\right)\in U$$
51	2 33 46 48 50	setchom	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to F\left(X\right)\mathrm{Hom}\left(S\right)F\left(Y\right)={F\left(Y\right)}^{F\left(X\right)}$$
52	32 45 51	feq123d	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(\left(XGY\right):X\mathrm{Hom}\left(E\right)Y⟶F\left(X\right)\mathrm{Hom}\left(S\right)F\left(Y\right)\leftrightarrow \left({\mathrm{I}\upharpoonright }_{\left({{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}\right)}\right):{{\mathrm{Base}}_Y}^{{\mathrm{Base}}_X}⟶{F\left(Y\right)}^{F\left(X\right)}\right)$$
53	29 52	mpbird	$$⊢\left(\phi \wedge \left(X\in B\wedge Y\in B\right)\right)\to \left(XGY\right):X\mathrm{Hom}\left(E\right)Y⟶F\left(X\right)\mathrm{Hom}\left(S\right)F\left(Y\right)$$