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

Proof

Step	Hyp	Ref	Expression
1		2str1.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ 𝑁 , + ⟩ }
2		2str1.b	⊢ ( Base ‘ ndx ) < 𝑁
3		2str1.n	⊢ 𝑁 ∈ ℕ
4		2str1.e	⊢ 𝐸 = Slot 𝑁
5	1 2 3	2strstr1	⊢ 𝐺 Struct ⟨ ( Base ‘ ndx ) , 𝑁 ⟩
6	4 3	ndxid	⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
7		snsspr2	⊢ { ⟨ 𝑁 , + ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ 𝑁 , + ⟩ }
8	4 3	ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝑁
9	8	opeq1i	⊢ ⟨ ( 𝐸 ‘ ndx ) , + ⟩ = ⟨ 𝑁 , + ⟩
10	9	sneqi	⊢ { ⟨ ( 𝐸 ‘ ndx ) , + ⟩ } = { ⟨ 𝑁 , + ⟩ }
11	7 10 1	3sstr4i	⊢ { ⟨ ( 𝐸 ‘ ndx ) , + ⟩ } ⊆ 𝐺
12	5 6 11	strfv	⊢ ( + ∈ 𝑉 → + = ( 𝐸 ‘ 𝐺 ) )