Theorem 2strstr

Description: A constructed two-slot structure. Depending on hard-coded indices. Use 2strstr1 instead. (Contributed by Mario Carneiro, 29-Aug-2015) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		2str.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( 𝐸 ‘ ndx ) , + ⟩ }
2		2str.e	⊢ 𝐸 = Slot 𝑁
3		2str.l	⊢ 1 < 𝑁
4		2str.n	⊢ 𝑁 ∈ ℕ
5		1nn	⊢ 1 ∈ ℕ
6		basendx	⊢ ( Base ‘ ndx ) = 1
7	2 4	ndxarg	⊢ ( 𝐸 ‘ ndx ) = 𝑁
8	5 6 3 4 7	strle2	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( 𝐸 ‘ ndx ) , + ⟩ } Struct ⟨ 1 , 𝑁 ⟩
9	1 8	eqbrtri	⊢ 𝐺 Struct ⟨ 1 , 𝑁 ⟩