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

Metamath Proof Explorer

Theorem hashprb

Description: The size of an unordered pair is 2 if and only if its elements are different sets. (Contributed by Alexander van der Vekens, 17-Jan-2018)

Ref Expression
Assertion hashprb 
|- ( ( M e. _V /\ N e. _V /\ M =/= N ) <-> ( # ` { M , N } ) = 2 )

Proof

Step Hyp Ref Expression
1 hashprg 
 |-  ( ( M e. _V /\ N e. _V ) -> ( M =/= N <-> ( # ` { M , N } ) = 2 ) )
2 1 biimp3a 
 |-  ( ( M e. _V /\ N e. _V /\ M =/= N ) -> ( # ` { M , N } ) = 2 )
3 elprchashprn2 
 |-  ( -. M e. _V -> -. ( # ` { M , N } ) = 2 )
4 pm2.21 
 |-  ( -. ( # ` { M , N } ) = 2 -> ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) ) )
5 3 4 syl 
 |-  ( -. M e. _V -> ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) ) )
6 elprchashprn2 
 |-  ( -. N e. _V -> -. ( # ` { N , M } ) = 2 )
7 prcom 
 |-  { N , M } = { M , N }
8 7 fveq2i 
 |-  ( # ` { N , M } ) = ( # ` { M , N } )
9 8 eqeq1i 
 |-  ( ( # ` { N , M } ) = 2 <-> ( # ` { M , N } ) = 2 )
10 9 4 sylnbi 
 |-  ( -. ( # ` { N , M } ) = 2 -> ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) ) )
11 6 10 syl 
 |-  ( -. N e. _V -> ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) ) )
12 simpll 
 |-  ( ( ( M e. _V /\ N e. _V ) /\ ( # ` { M , N } ) = 2 ) -> M e. _V )
13 simplr 
 |-  ( ( ( M e. _V /\ N e. _V ) /\ ( # ` { M , N } ) = 2 ) -> N e. _V )
14 1 biimpar 
 |-  ( ( ( M e. _V /\ N e. _V ) /\ ( # ` { M , N } ) = 2 ) -> M =/= N )
15 12 13 14 3jca 
 |-  ( ( ( M e. _V /\ N e. _V ) /\ ( # ` { M , N } ) = 2 ) -> ( M e. _V /\ N e. _V /\ M =/= N ) )
16 15 ex 
 |-  ( ( M e. _V /\ N e. _V ) -> ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) ) )
17 5 11 16 ecase 
 |-  ( ( # ` { M , N } ) = 2 -> ( M e. _V /\ N e. _V /\ M =/= N ) )
18 2 17 impbii 
 |-  ( ( M e. _V /\ N e. _V /\ M =/= N ) <-> ( # ` { M , N } ) = 2 )