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 syl6eq ⟨“ 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