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	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( 𝐸 ‘ ndx ) , + ⟩ }
	2str.e	⊢ 𝐸 = Slot 𝑁
	2str.l	⊢ 1 < 𝑁
	2str.n	⊢ 𝑁 ∈ ℕ
Assertion	2strop	⊢ ( + ∈ 𝑉 → + = ( 𝐸 ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		2str.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( 𝐸 ‘ ndx ) , + ⟩ }
2		2str.e	⊢ 𝐸 = Slot 𝑁
3		2str.l	⊢ 1 < 𝑁
4		2str.n	⊢ 𝑁 ∈ ℕ
5	1 2 3 4	2strstr	⊢ 𝐺 Struct ⟨ 1 , 𝑁 ⟩
6	2 4	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
7		snsspr2	⊢ { ⟨ ( 𝐸 ‘ ndx ) , + ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( 𝐸 ‘ ndx ) , + ⟩ }
8	7 1	sseqtrri	⊢ { ⟨ ( 𝐸 ‘ ndx ) , + ⟩ } ⊆ 𝐺
9	5 6 8	strfv	⊢ ( + ∈ 𝑉 → + = ( 𝐸 ‘ 𝐺 ) )