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