Theorem 2strbas

Description: The base set 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	⊢ 𝑁 ∈ ℕ
Assertion	2strbas	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐺 ) )

Proof

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