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}⟨“AB”⟩=\left\{0,1\right\}$$

Proof

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