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 } )