Theorem funcsetcestrclem1

Description: Lemma 1 for funcsetcestrc . (Contributed by AV, 27-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)$$
Assertion	funcsetcestrclem1	$$⊢\left(\phi \wedge X\in C\right)\to F\left(X\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}$$

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	3	adantr	$$⊢\left(\phi \wedge X\in C\right)\to F=\left(x\in C⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x⟩\right\}\right)$$
5		opeq2	$$⊢x=X\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},x⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩$$
6	5	sneqd	$$⊢x=X\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}$$
7	6	adantl	$$⊢\left(\left(\phi \wedge X\in C\right)\wedge x=X\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}$$
8		simpr	$$⊢\left(\phi \wedge X\in C\right)\to X\in C$$
9		snex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}\in \mathrm{V}$$
10	9	a1i	$$⊢\left(\phi \wedge X\in C\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}\in \mathrm{V}$$
11	4 7 8 10	fvmptd	$$⊢\left(\phi \wedge X\in C\right)\to F\left(X\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X⟩\right\}$$