Metamath Proof Explorer

Theorem s2dm

Description: The domain of a doubleton word is an unordered pair. (Contributed by AV, 9-Jan-2020)

Ref Expression
Assertion s2dm ⊢ dom ⁡ ⟨“ AB ”⟩ = 0 1

Proof

Step Hyp Ref Expression
1 s2cli ⊢ ⟨“ AB ”⟩ ∈ Word V
2 wrdf ⊢ ⟨“ AB ”⟩ ∈ Word V → ⟨“ AB ”⟩ : 0 ..^ ⟨“ AB ”⟩ ⟶ V
3 1 2 ax-mp ⊢ ⟨“ AB ”⟩ : 0 ..^ ⟨“ AB ”⟩ ⟶ V
4 s2len ⊢ ⟨“ AB ”⟩ = 2
5 oveq2 ⊢ ⟨“ AB ”⟩ = 2 → 0 ..^ ⟨“ AB ”⟩ = 0 ..^ 2
6 fzo0to2pr ⊢ 0 ..^ 2 = 0 1
7 5 6 eqtrdi ⊢ ⟨“ AB ”⟩ = 2 → 0 ..^ ⟨“ AB ”⟩ = 0 1
8 4 7 ax-mp ⊢ 0 ..^ ⟨“ AB ”⟩ = 0 1
9 8 feq2i ⊢ ⟨“ AB ”⟩ : 0 ..^ ⟨“ AB ”⟩ ⟶ V ↔ ⟨“ AB ”⟩ : 0 1 ⟶ V
10 3 9 mpbi ⊢ ⟨“ AB ”⟩ : 0 1 ⟶ V
11 10 fdmi ⊢ dom ⁡ ⟨“ AB ”⟩ = 0 1