Theorem 2strop1

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

	Ref	Expression
Hypotheses	2str1.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨N,\underset{\dot{}}{+}⟩\right\}$$
	2str1.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<N$$
	2str1.n	$$⊢N\in \mathbb{N}$$
	2str1.e	$$⊢E=\mathrm{Slot}N$$
Assertion	2strop1	$$⊢\underset{\dot{}}{+}\in V\to \underset{\dot{}}{+}=E\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		2str1.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨N,\underset{\dot{}}{+}⟩\right\}$$
2		2str1.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<N$$
3		2str1.n	$$⊢N\in \mathbb{N}$$
4		2str1.e	$$⊢E=\mathrm{Slot}N$$
5	1 2 3	2strstr1	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},N⟩$$
6	4 3	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
7		snsspr2	$$⊢\left\{⟨N,\underset{\dot{}}{+}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨N,\underset{\dot{}}{+}⟩\right\}$$
8	4 3	ndxarg	$$⊢E\left(\mathrm{ndx}\right)=N$$
9	8	opeq1i	$$⊢⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩=⟨N,\underset{\dot{}}{+}⟩$$
10	9	sneqi	$$⊢\left\{⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}=\left\{⟨N,\underset{\dot{}}{+}⟩\right\}$$
11	7 10 1	3sstr4i	$$⊢\left\{⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}\subseteq G$$
12	5 6 11	strfv	$$⊢\underset{\dot{}}{+}\in V\to \underset{\dot{}}{+}=E\left(G\right)$$