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 )