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

Metamath Proof Explorer

Theorem snopiswrd

Description: A singleton of an ordered pair (with 0 as first component) is a word. (Contributed by AV, 23-Nov-2018) (Proof shortened by AV, 18-Apr-2021)

		Ref	Expression
	Assertion	snopiswrd	$⊢ S \in V \to \{⟨0, S⟩\} \in Word V$

Proof

Step	Hyp	Ref	Expression
1		0zd	$⊢ S \in V \to 0 \in ℤ$
2		id	$⊢ S \in V \to S \in V$
3	1 2	fsnd	$⊢ S \in V \to \{⟨0, S⟩\} : \{0\} ⟶ V$
4		fzo01	$⊢ (0 ..^1) = \{0\}$
5	4	feq2i	$⊢ \{⟨0, S⟩\} : (0 ..^1) ⟶ V \leftrightarrow \{⟨0, S⟩\} : \{0\} ⟶ V$
6	3 5	sylibr	$⊢ S \in V \to \{⟨0, S⟩\} : (0 ..^1) ⟶ V$
7		iswrdi	$⊢ \{⟨0, S⟩\} : (0 ..^1) ⟶ V \to \{⟨0, S⟩\} \in Word V$
8	6 7	syl	$⊢ S \in V \to \{⟨0, S⟩\} \in Word V$