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 <" A B "> = { 0 , 1 }

Proof

Step Hyp Ref Expression
1 s2cli 
 |-  <" A B "> e. Word _V
2 wrdf 
 |-  ( <" A B "> e. Word _V -> <" A B "> : ( 0 ..^ ( # ` <" A B "> ) ) --> _V )
3 1 2 ax-mp 
 |-  <" A B "> : ( 0 ..^ ( # ` <" A B "> ) ) --> _V
4 s2len 
 |-  ( # ` <" A B "> ) = 2
5 oveq2 
 |-  ( ( # ` <" A B "> ) = 2 -> ( 0 ..^ ( # ` <" A B "> ) ) = ( 0 ..^ 2 ) )
6 fzo0to2pr 
 |-  ( 0 ..^ 2 ) = { 0 , 1 }
7 5 6 eqtrdi 
 |-  ( ( # ` <" A B "> ) = 2 -> ( 0 ..^ ( # ` <" A B "> ) ) = { 0 , 1 } )
8 4 7 ax-mp 
 |-  ( 0 ..^ ( # ` <" A B "> ) ) = { 0 , 1 }
9 8 feq2i 
 |-  ( <" A B "> : ( 0 ..^ ( # ` <" A B "> ) ) --> _V <-> <" A B "> : { 0 , 1 } --> _V )
10 3 9 mpbi 
 |-  <" A B "> : { 0 , 1 } --> _V
11 10 fdmi 
 |-  dom <" A B "> = { 0 , 1 }