Theorem embedsetcestrclem

Description: Lemma for embedsetcestrc . (Contributed by AV, 31-Mar-2020)

	Ref	Expression
Hypotheses	funcsetcestrc.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
	funcsetcestrc.c	$$⊢C={\mathrm{Base}}_S$$
	funcsetcestrc.f	$$⊢\phi \to F=\left(x\in C⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x⟩\right\}\right)$$
	funcsetcestrc.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	funcsetcestrc.o	$$⊢\phi \to \mathrm{\omega }\in U$$
	funcsetcestrclem3.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
	funcsetcestrclem3.b	$$⊢B={\mathrm{Base}}_E$$
Assertion	embedsetcestrclem	$$⊢\phi \to F:C\underset{1-1}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		funcsetcestrc.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
2		funcsetcestrc.c	$$⊢C={\mathrm{Base}}_S$$
3		funcsetcestrc.f	$$⊢\phi \to F=\left(x\in C⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x⟩\right\}\right)$$
4		funcsetcestrc.u	$$⊢\phi \to U\in \mathrm{WUni}$$
5		funcsetcestrc.o	$$⊢\phi \to \mathrm{\omega }\in U$$
6		funcsetcestrclem3.e	$$⊢E=\mathrm{ExtStrCat}\left(U\right)$$
7		funcsetcestrclem3.b	$$⊢B={\mathrm{Base}}_E$$
8	1 2 3 4 5 6 7	funcsetcestrclem3	$$⊢\phi \to F:C⟶B$$
9	1 2 3	funcsetcestrclem1	$$⊢\left(\phi \wedge y\in C\right)\to F\left(y\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩\right\}$$
10	9	adantrr	$$⊢\left(\phi \wedge \left(y\in C\wedge z\in C\right)\right)\to F\left(y\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩\right\}$$
11	1 2 3	funcsetcestrclem1	$$⊢\left(\phi \wedge z\in C\right)\to F\left(z\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},z⟩\right\}$$
12	11	adantrl	$$⊢\left(\phi \wedge \left(y\in C\wedge z\in C\right)\right)\to F\left(z\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},z⟩\right\}$$
13	10 12	eqeq12d	$$⊢\left(\phi \wedge \left(y\in C\wedge z\in C\right)\right)\to \left(F\left(y\right)=F\left(z\right)\leftrightarrow \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},z⟩\right\}\right)$$
14		opex	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩\in \mathrm{V}$$
15		sneqbg	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩\in \mathrm{V}\to \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},z⟩\right\}\leftrightarrow ⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},z⟩\right)$$
16	14 15	mp1i	$$⊢\left(\phi \wedge \left(y\in C\wedge z\in C\right)\right)\to \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},z⟩\right\}\leftrightarrow ⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},z⟩\right)$$
17		fvexd	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
18		simpl	$$⊢\left(y\in C\wedge z\in C\right)\to y\in C$$
19		opthg	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}\wedge y\in C\right)\to \left(⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},z⟩\leftrightarrow \left({\mathrm{Base}}_{\mathrm{ndx}}={\mathrm{Base}}_{\mathrm{ndx}}\wedge y=z\right)\right)$$
20	17 18 19	syl2an	$$⊢\left(\phi \wedge \left(y\in C\wedge z\in C\right)\right)\to \left(⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},z⟩\leftrightarrow \left({\mathrm{Base}}_{\mathrm{ndx}}={\mathrm{Base}}_{\mathrm{ndx}}\wedge y=z\right)\right)$$
21		simpr	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}={\mathrm{Base}}_{\mathrm{ndx}}\wedge y=z\right)\to y=z$$
22	20 21	syl6bi	$$⊢\left(\phi \wedge \left(y\in C\wedge z\in C\right)\right)\to \left(⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},z⟩\to y=z\right)$$
23	16 22	sylbid	$$⊢\left(\phi \wedge \left(y\in C\wedge z\in C\right)\right)\to \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},y⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},z⟩\right\}\to y=z\right)$$
24	13 23	sylbid	$$⊢\left(\phi \wedge \left(y\in C\wedge z\in C\right)\right)\to \left(F\left(y\right)=F\left(z\right)\to y=z\right)$$
25	24	ralrimivva	$$⊢\phi \to \forall y\in C\forall z\in C\left(F\left(y\right)=F\left(z\right)\to y=z\right)$$
26		dff13	$$⊢F:C\underset{1-1}{⟶}B\leftrightarrow \left(F:C⟶B\wedge \forall y\in C\forall z\in C\left(F\left(y\right)=F\left(z\right)\to y=z\right)\right)$$
27	8 25 26	sylanbrc	$$⊢\phi \to F:C\underset{1-1}{⟶}B$$