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

Metamath Proof Explorer

Theorem f1o2sn

Description: A singleton consisting in a nested ordered pair is a one-to-one function from the cartesian product of two singletons onto a singleton (case where the two singletons are equal). (Contributed by AV, 15-Aug-2019)

Ref Expression
Assertion f1o2sn 
|- ( ( E e. V /\ X e. W ) -> { <. <. E , E >. , X >. } : ( { E } X. { E } ) -1-1-onto-> { X } )

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. E , E >. e. _V
2 simpr 
 |-  ( ( E e. V /\ X e. W ) -> X e. W )
3 f1osng 
 |-  ( ( <. E , E >. e. _V /\ X e. W ) -> { <. <. E , E >. , X >. } : { <. E , E >. } -1-1-onto-> { X } )
4 1 2 3 sylancr 
 |-  ( ( E e. V /\ X e. W ) -> { <. <. E , E >. , X >. } : { <. E , E >. } -1-1-onto-> { X } )
5 xpsng 
 |-  ( ( E e. V /\ E e. V ) -> ( { E } X. { E } ) = { <. E , E >. } )
6 5 anidms 
 |-  ( E e. V -> ( { E } X. { E } ) = { <. E , E >. } )
7 6 eqcomd 
 |-  ( E e. V -> { <. E , E >. } = ( { E } X. { E } ) )
8 7 adantr 
 |-  ( ( E e. V /\ X e. W ) -> { <. E , E >. } = ( { E } X. { E } ) )
9 8 f1oeq2d 
 |-  ( ( E e. V /\ X e. W ) -> ( { <. <. E , E >. , X >. } : { <. E , E >. } -1-1-onto-> { X } <-> { <. <. E , E >. , X >. } : ( { E } X. { E } ) -1-1-onto-> { X } ) )
10 4 9 mpbid 
 |-  ( ( E e. V /\ X e. W ) -> { <. <. E , E >. , X >. } : ( { E } X. { E } ) -1-1-onto-> { X } )