Metamath Proof Explorer

Theorem s111

Description: The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015) (Revised by Mario Carneiro, 26-Feb-2016)

Ref Expression
Assertion s111 
|- ( ( S e. A /\ T e. A ) -> ( <" S "> = <" T "> <-> S = T ) )

Proof

Step Hyp Ref Expression
1 s1val 
 |-  ( S e. A -> <" S "> = { <. 0 , S >. } )
2 s1val 
 |-  ( T e. A -> <" T "> = { <. 0 , T >. } )
3 1 2 eqeqan12d 
 |-  ( ( S e. A /\ T e. A ) -> ( <" S "> = <" T "> <-> { <. 0 , S >. } = { <. 0 , T >. } ) )
4 opex 
 |-  <. 0 , S >. e. _V
5 sneqbg 
 |-  ( <. 0 , S >. e. _V -> ( { <. 0 , S >. } = { <. 0 , T >. } <-> <. 0 , S >. = <. 0 , T >. ) )
6 4 5 mp1i 
 |-  ( ( S e. A /\ T e. A ) -> ( { <. 0 , S >. } = { <. 0 , T >. } <-> <. 0 , S >. = <. 0 , T >. ) )
7 0z 
 |-  0 e. ZZ
8 eqid 
 |-  0 = 0
9 opthg 
 |-  ( ( 0 e. ZZ /\ S e. A ) -> ( <. 0 , S >. = <. 0 , T >. <-> ( 0 = 0 /\ S = T ) ) )
10 9 baibd 
 |-  ( ( ( 0 e. ZZ /\ S e. A ) /\ 0 = 0 ) -> ( <. 0 , S >. = <. 0 , T >. <-> S = T ) )
11 8 10 mpan2 
 |-  ( ( 0 e. ZZ /\ S e. A ) -> ( <. 0 , S >. = <. 0 , T >. <-> S = T ) )
12 7 11 mpan 
 |-  ( S e. A -> ( <. 0 , S >. = <. 0 , T >. <-> S = T ) )
13 12 adantr 
 |-  ( ( S e. A /\ T e. A ) -> ( <. 0 , S >. = <. 0 , T >. <-> S = T ) )
14 3 6 13 3bitrd 
 |-  ( ( S e. A /\ T e. A ) -> ( <" S "> = <" T "> <-> S = T ) )