Theorem 2strbas

Description: The base set of a constructed two-slot structure not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020)

	Ref	Expression
Hypotheses	2str.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨N,\underset{\dot{}}{+}⟩\right\}$$
	2str.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<N$$
	2str.n	$$⊢N\in \mathbb{N}$$
Assertion	2strbas	$$⊢B\in V\to B={\mathrm{Base}}_G$$

Proof

Step	Hyp	Ref	Expression
1		2str.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨N,\underset{\dot{}}{+}⟩\right\}$$
2		2str.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<N$$
3		2str.n	$$⊢N\in \mathbb{N}$$
4	1 2 3	2strstr	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},N⟩$$
5		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
6		snsspr1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨N,\underset{\dot{}}{+}⟩\right\}$$
7	6 1	sseqtrri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}\subseteq G$$
8	4 5 7	strfv	$$⊢B\in V\to B={\mathrm{Base}}_G$$