Metamath Proof Explorer

Theorem wrd3tpop

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

Ref Expression
Assertion wrd3tpop ⊢ W ∈ Word V ∧ W = 3 → W = 0 W ⁡ 0 1 W ⁡ 1 2 W ⁡ 2

Proof

Step Hyp Ref Expression
1 wrdfn ⊢ W ∈ Word V → W Fn 0 ..^ W
2 1 adantr ⊢ W ∈ Word V ∧ W = 3 → W Fn 0 ..^ W
3 oveq2 ⊢ W = 3 → 0 ..^ W = 0 ..^ 3
4 fzo0to3tp ⊢ 0 ..^ 3 = 0 1 2
5 3 4 eqtr2di ⊢ W = 3 → 0 1 2 = 0 ..^ W
6 5 adantl ⊢ W ∈ Word V ∧ W = 3 → 0 1 2 = 0 ..^ W
7 6 fneq2d ⊢ W ∈ Word V ∧ W = 3 → W Fn 0 1 2 ↔ W Fn 0 ..^ W
8 2 7 mpbird ⊢ W ∈ Word V ∧ W = 3 → W Fn 0 1 2
9 c0ex ⊢ 0 ∈ V
10 1ex ⊢ 1 ∈ V
11 2ex ⊢ 2 ∈ V
12 9 10 11 fntpb ⊢ W Fn 0 1 2 ↔ W = 0 W ⁡ 0 1 W ⁡ 1 2 W ⁡ 2
13 8 12 sylib ⊢ W ∈ Word V ∧ W = 3 → W = 0 W ⁡ 0 1 W ⁡ 1 2 W ⁡ 2