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 ${⊢}\mathrm{dom}⟨“{A}{B}”⟩=\left\{0,1\right\}$

Proof

Step Hyp Ref Expression
1 s2cli ${⊢}⟨“{A}{B}”⟩\in \mathrm{Word}\mathrm{V}$
2 wrdf ${⊢}⟨“{A}{B}”⟩\in \mathrm{Word}\mathrm{V}\to ⟨“{A}{B}”⟩:\left(0..^\left|⟨“{A}{B}”⟩\right|\right)⟶\mathrm{V}$
3 1 2 ax-mp ${⊢}⟨“{A}{B}”⟩:\left(0..^\left|⟨“{A}{B}”⟩\right|\right)⟶\mathrm{V}$
4 s2len ${⊢}\left|⟨“{A}{B}”⟩\right|=2$
5 oveq2 ${⊢}\left|⟨“{A}{B}”⟩\right|=2\to \left(0..^\left|⟨“{A}{B}”⟩\right|\right)=\left(0..^2\right)$
6 fzo0to2pr ${⊢}\left(0..^2\right)=\left\{0,1\right\}$
7 5 6 syl6eq ${⊢}\left|⟨“{A}{B}”⟩\right|=2\to \left(0..^\left|⟨“{A}{B}”⟩\right|\right)=\left\{0,1\right\}$
8 4 7 ax-mp ${⊢}\left(0..^\left|⟨“{A}{B}”⟩\right|\right)=\left\{0,1\right\}$
9 8 feq2i ${⊢}⟨“{A}{B}”⟩:\left(0..^\left|⟨“{A}{B}”⟩\right|\right)⟶\mathrm{V}↔⟨“{A}{B}”⟩:\left\{0,1\right\}⟶\mathrm{V}$
10 3 9 mpbi ${⊢}⟨“{A}{B}”⟩:\left\{0,1\right\}⟶\mathrm{V}$
11 10 fdmi ${⊢}\mathrm{dom}⟨“{A}{B}”⟩=\left\{0,1\right\}$