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

Metamath Proof Explorer

Theorem 1strstr

Description: A constructed one-slot structure. (Contributed by AV, 15-Nov-2024)

		Ref	Expression
	Hypothesis	1str.g	$⊢ G = \{⟨{Base}_{ndx}, B⟩\}$
	Assertion	1strstr	$⊢ G Struct ⟨{Base}_{ndx}, {Base}_{ndx}⟩$

Step	Hyp	Ref	Expression
1		1str.g	$⊢ G = \{⟨{Base}_{ndx}, B⟩\}$
2		basendxnn	$⊢ {Base}_{ndx} \in ℕ$
3		eqid	$⊢ {Base}_{ndx} = {Base}_{ndx}$
4	2 3	strle1	$⊢ \{⟨{Base}_{ndx}, B⟩\} Struct ⟨{Base}_{ndx}, {Base}_{ndx}⟩$
5	1 4	eqbrtri	$⊢ G Struct ⟨{Base}_{ndx}, {Base}_{ndx}⟩$