Theorem 2strbas

Description: The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015) Use the index-independent version 2strbas1 instead. (New usage is discouraged.)

	Ref	Expression
Hypotheses	2str.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}$$
	2str.e	$$⊢E=\mathrm{Slot}N$$
	2str.l	$$⊢1<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⟩,⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}$$
2		2str.e	$$⊢E=\mathrm{Slot}N$$
3		2str.l	$$⊢1<N$$
4		2str.n	$$⊢N\in \mathbb{N}$$
5	1 2 3 4	2strstr	$$⊢G\mathrm{Struct}⟨1,N⟩$$
6		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
7		snsspr1	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}$$
8	7 1	sseqtrri	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩\right\}\subseteq G$$
9	5 6 8	strfv	$$⊢B\in V\to B={\mathrm{Base}}_G$$