Metamath Proof Explorer

Theorem wrd2pr2op

Description: A word of length two represented as unordered pair of ordered pairs. (Contributed by AV, 20-Oct-2018) (Proof shortened by AV, 26-Jan-2021)

		Ref	Expression
	Assertion	wrd2pr2op	$⊢ (W \in Word V \land \|W\| = 2) \to W = \{⟨0, W (0)⟩, ⟨1, W (1)⟩\}$

Proof

Step	Hyp	Ref	Expression
1		wrdfn	$⊢ W \in Word V \to W Fn (0 ..^\|W\|)$
2	1	adantr	$⊢ (W \in Word V \land \|W\| = 2) \to W Fn (0 ..^\|W\|)$
3		oveq2	$⊢ \|W\| = 2 \to (0 ..^\|W\|) = (0 ..^2)$
4		fzo0to2pr	$⊢ (0 ..^2) = \{0, 1\}$
5	3 4	eqtr2di	$⊢ \|W\| = 2 \to \{0, 1\} = (0 ..^\|W\|)$
6	5	adantl	$⊢ (W \in Word V \land \|W\| = 2) \to \{0, 1\} = (0 ..^\|W\|)$
7	6	fneq2d	$⊢ (W \in Word V \land \|W\| = 2) \to (W Fn \{0, 1\} \leftrightarrow W Fn (0 ..^\|W\|))$
8	2 7	mpbird	$⊢ (W \in Word V \land \|W\| = 2) \to W Fn \{0, 1\}$
9		c0ex	$⊢ 0 \in V$
10		1ex	$⊢ 1 \in V$
11	9 10	fnprb	$⊢ W Fn \{0, 1\} \leftrightarrow W = \{⟨0, W (0)⟩, ⟨1, W (1)⟩\}$
12	8 11	sylib	$⊢ (W \in Word V \land \|W\| = 2) \to W = \{⟨0, W (0)⟩, ⟨1, W (1)⟩\}$