Theorem 2strbas

Description: The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015) Use the index-independent version 2strbas1 instead. (New usage is discouraged.)

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

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		baseid	⊢ Base = Slot ( Base ‘ ndx )
7		snsspr1	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( 𝐸 ‘ ndx ) , + ⟩ }
8	7 1	sseqtrri	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ } ⊆ 𝐺
9	5 6 8	strfv	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 = ( Base ‘ 𝐺 ) )