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 ∈ Word V ∧ W = 2 → W = 0 W ⁡ 0 1 W ⁡ 1

Proof

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