Metamath Proof Explorer

Theorem elprchashprn2

Description: If one element of an unordered pair is not a set, the size of the unordered pair is not 2. (Contributed by Alexander van der Vekens, 7-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 prprc1 
 |-  ( -. M e. _V -> { M , N } = { N } )
2 hashsng 
 |-  ( N e. _V -> ( # ` { N } ) = 1 )
3 fveq2 
 |-  ( { M , N } = { N } -> ( # ` { M , N } ) = ( # ` { N } ) )
4 3 eqcomd 
 |-  ( { M , N } = { N } -> ( # ` { N } ) = ( # ` { M , N } ) )
5 4 eqeq1d 
 |-  ( { M , N } = { N } -> ( ( # ` { N } ) = 1 <-> ( # ` { M , N } ) = 1 ) )
6 5 biimpa 
 |-  ( ( { M , N } = { N } /\ ( # ` { N } ) = 1 ) -> ( # ` { M , N } ) = 1 )
7 id 
 |-  ( ( # ` { M , N } ) = 1 -> ( # ` { M , N } ) = 1 )
8 1ne2 
 |-  1 =/= 2
9 8 a1i 
 |-  ( ( # ` { M , N } ) = 1 -> 1 =/= 2 )
10 7 9 eqnetrd 
 |-  ( ( # ` { M , N } ) = 1 -> ( # ` { M , N } ) =/= 2 )
11 10 neneqd 
 |-  ( ( # ` { M , N } ) = 1 -> -. ( # ` { M , N } ) = 2 )
12 6 11 syl 
 |-  ( ( { M , N } = { N } /\ ( # ` { N } ) = 1 ) -> -. ( # ` { M , N } ) = 2 )
13 12 expcom 
 |-  ( ( # ` { N } ) = 1 -> ( { M , N } = { N } -> -. ( # ` { M , N } ) = 2 ) )
14 2 13 syl 
 |-  ( N e. _V -> ( { M , N } = { N } -> -. ( # ` { M , N } ) = 2 ) )
15 snprc 
 |-  ( -. N e. _V <-> { N } = (/) )
16 eqeq2 
 |-  ( { N } = (/) -> ( { M , N } = { N } <-> { M , N } = (/) ) )
17 16 biimpa 
 |-  ( ( { N } = (/) /\ { M , N } = { N } ) -> { M , N } = (/) )
18 hash0 
 |-  ( # ` (/) ) = 0
19 fveq2 
 |-  ( { M , N } = (/) -> ( # ` { M , N } ) = ( # ` (/) ) )
20 19 eqcomd 
 |-  ( { M , N } = (/) -> ( # ` (/) ) = ( # ` { M , N } ) )
21 20 eqeq1d 
 |-  ( { M , N } = (/) -> ( ( # ` (/) ) = 0 <-> ( # ` { M , N } ) = 0 ) )
22 21 biimpa 
 |-  ( ( { M , N } = (/) /\ ( # ` (/) ) = 0 ) -> ( # ` { M , N } ) = 0 )
23 id 
 |-  ( ( # ` { M , N } ) = 0 -> ( # ` { M , N } ) = 0 )
24 0ne2 
 |-  0 =/= 2
25 24 a1i 
 |-  ( ( # ` { M , N } ) = 0 -> 0 =/= 2 )
26 23 25 eqnetrd 
 |-  ( ( # ` { M , N } ) = 0 -> ( # ` { M , N } ) =/= 2 )
27 26 neneqd 
 |-  ( ( # ` { M , N } ) = 0 -> -. ( # ` { M , N } ) = 2 )
28 22 27 syl 
 |-  ( ( { M , N } = (/) /\ ( # ` (/) ) = 0 ) -> -. ( # ` { M , N } ) = 2 )
29 17 18 28 sylancl 
 |-  ( ( { N } = (/) /\ { M , N } = { N } ) -> -. ( # ` { M , N } ) = 2 )
30 29 ex 
 |-  ( { N } = (/) -> ( { M , N } = { N } -> -. ( # ` { M , N } ) = 2 ) )
31 15 30 sylbi 
 |-  ( -. N e. _V -> ( { M , N } = { N } -> -. ( # ` { M , N } ) = 2 ) )
32 14 31 pm2.61i 
 |-  ( { M , N } = { N } -> -. ( # ` { M , N } ) = 2 )
33 1 32 syl 
 |-  ( -. M e. _V -> -. ( # ` { M , N } ) = 2 )