Theorem estrreslem1

Description: Lemma 1 for estrres . (Contributed by AV, 14-Mar-2020)

	Ref	Expression
Hypotheses	estrres.c	$$⊢\phi \to C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
	estrres.b	$$⊢\phi \to B\in V$$
Assertion	estrreslem1	$$⊢\phi \to B={\mathrm{Base}}_C$$

Proof

Step	Hyp	Ref	Expression
1		estrres.c	$$⊢\phi \to C=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}$$
2		estrres.b	$$⊢\phi \to B\in V$$
3	1	fveq2d	$$⊢\phi \to {\mathrm{Base}}_C={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}}$$
4		tpex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\in \mathrm{V}$$
5	4	a1i	$$⊢\phi \to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\in \mathrm{V}$$
6		df-base	$$⊢\mathrm{Base}=\mathrm{Slot}1$$
7		1nn	$$⊢1\in \mathbb{N}$$
8	5 6 7	strndxid	$$⊢\phi \to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\left({\mathrm{Base}}_{\mathrm{ndx}}\right)={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}}$$
9		fvexd	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
10		slotsbhcdif	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$$
11		3simpa	$$⊢\left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\wedge \mathrm{Hom}\left(\mathrm{ndx}\right)\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)\to \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$$
12	10 11	mp1i	$$⊢\phi \to \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)$$
13		fvtp1g	$$⊢\left(\left({\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}\wedge B\in V\right)\wedge \left({\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{Hom}\left(\mathrm{ndx}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{comp}\left(\mathrm{ndx}\right)\right)\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\left({\mathrm{Base}}_{\mathrm{ndx}}\right)=B$$
14	9 2 12 13	syl21anc	$$⊢\phi \to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),H⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\underset{\dot{}}{·}⟩\right\}\left({\mathrm{Base}}_{\mathrm{ndx}}\right)=B$$
15	3 8 14	3eqtr2rd	$$⊢\phi \to B={\mathrm{Base}}_C$$