This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⟨“ 𝐴 𝐵 ”⟩ = { 0 , 1 }

Proof

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