Theorem 2strop

Description: The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015) Use the index-independent version 2strop1 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	2strop	$$⊢\underset{\dot{}}{+}\in V\to \underset{\dot{}}{+}=E\left(G\right)$$

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	2 4	ndxid	$$⊢E=\mathrm{Slot}E\left(\mathrm{ndx}\right)$$
7		snsspr2	$$⊢\left\{⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}\subseteq \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}$$
8	7 1	sseqtrri	$$⊢\left\{⟨E\left(\mathrm{ndx}\right),\underset{\dot{}}{+}⟩\right\}\subseteq G$$
9	5 6 8	strfv	$$⊢\underset{\dot{}}{+}\in V\to \underset{\dot{}}{+}=E\left(G\right)$$