wrd3tpop

Description: A word of length three represented as triple of ordered pairs. (Contributed by AV, 26-Jan-2021)

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

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

Metamath Proof Explorer