Theorem funcestrcsetclem2

Description: Lemma 2 for funcestrcsetc . (Contributed by AV, 22-Mar-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)$$
Assertion	funcestrcsetclem2	$$⊢\left(\phi \wedge X\in B\right)\to F\left(X\right)\in U$$

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	1 2 3 4 5 6	funcestrcsetclem1	$$⊢\left(\phi \wedge X\in B\right)\to F\left(X\right)={\mathrm{Base}}_X$$
8	1 3 5	estrcbasbas	$$⊢\left(\phi \wedge X\in B\right)\to {\mathrm{Base}}_X\in U$$
9	7 8	eqeltrd	$$⊢\left(\phi \wedge X\in B\right)\to F\left(X\right)\in U$$