repsw1

Description: The "repeated symbol word" of length 1. (Contributed by AV, 4-Nov-2018)

		Ref	Expression
	Assertion	repsw1	$⊢ S \in V \to S repeatS 1 = ⟨“ S ”⟩$

Step	Hyp	Ref	Expression
1		1nn0	$⊢ 1 \in ℕ_{0}$
2		repsconst	$⊢ (S \in V \land 1 \in ℕ_{0}) \to S repeatS 1 = (0 ..^1) \times \{S\}$
3	1 2	mpan2	$⊢ S \in V \to S repeatS 1 = (0 ..^1) \times \{S\}$
4		fzo01	$⊢ (0 ..^1) = \{0\}$
5	4	a1i	$⊢ S \in V \to (0 ..^1) = \{0\}$
6	5	xpeq1d	$⊢ S \in V \to (0 ..^1) \times \{S\} = \{0\} \times \{S\}$
7		c0ex	$⊢ 0 \in V$
8		xpsng	$⊢ (0 \in V \land S \in V) \to \{0\} \times \{S\} = \{⟨0, S⟩\}$
9	7 8	mpan	$⊢ S \in V \to \{0\} \times \{S\} = \{⟨0, S⟩\}$
10	3 6 9	3eqtrd	$⊢ S \in V \to S repeatS 1 = \{⟨0, S⟩\}$
11		s1val	$⊢ S \in V \to ⟨“ S ”⟩ = \{⟨0, S⟩\}$
12	10 11	eqtr4d	$⊢ S \in V \to S repeatS 1 = ⟨“ S ”⟩$

Metamath Proof Explorer