This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2strop

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

Ref Expression
Hypotheses 2str.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ 𝑁 , + ⟩ }
2str.b ⊢ ( Base ‘ ndx ) < 𝑁
2str.n ⊢ 𝑁 ∈ ℕ
2str.e ⊢ 𝐸 = Slot 𝑁
Assertion 2strop ( + ∈ 𝑉 → + = ( 𝐸 ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 2str.g ⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ 𝑁 , + ⟩ }
2 2str.b ⊢ ( Base ‘ ndx ) < 𝑁
3 2str.n ⊢ 𝑁 ∈ ℕ
4 2str.e ⊢ 𝐸 = Slot 𝑁
5 1 2 3 2strstr ⊢ 𝐺 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 ⊢ ( + ∈ 𝑉 → + = ( 𝐸 ‘ 𝐺 ) )