Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- { x e. { A } | ph } = { x e. { A } | ph } |
2 |
|
rabrsn |
|- ( { x e. { A } | ph } = { x e. { A } | ph } -> ( { x e. { A } | ph } = (/) \/ { x e. { A } | ph } = { A } ) ) |
3 |
|
fveqeq2 |
|- ( { x e. { A } | ph } = (/) -> ( ( # ` { x e. { A } | ph } ) = N <-> ( # ` (/) ) = N ) ) |
4 |
|
eqcom |
|- ( ( # ` (/) ) = N <-> N = ( # ` (/) ) ) |
5 |
4
|
biimpi |
|- ( ( # ` (/) ) = N -> N = ( # ` (/) ) ) |
6 |
|
hash0 |
|- ( # ` (/) ) = 0 |
7 |
5 6
|
eqtrdi |
|- ( ( # ` (/) ) = N -> N = 0 ) |
8 |
7
|
orcd |
|- ( ( # ` (/) ) = N -> ( N = 0 \/ N = 1 ) ) |
9 |
3 8
|
syl6bi |
|- ( { x e. { A } | ph } = (/) -> ( ( # ` { x e. { A } | ph } ) = N -> ( N = 0 \/ N = 1 ) ) ) |
10 |
|
fveqeq2 |
|- ( { x e. { A } | ph } = { A } -> ( ( # ` { x e. { A } | ph } ) = N <-> ( # ` { A } ) = N ) ) |
11 |
|
eqcom |
|- ( ( # ` { A } ) = N <-> N = ( # ` { A } ) ) |
12 |
11
|
biimpi |
|- ( ( # ` { A } ) = N -> N = ( # ` { A } ) ) |
13 |
|
hashsng |
|- ( A e. _V -> ( # ` { A } ) = 1 ) |
14 |
12 13
|
sylan9eqr |
|- ( ( A e. _V /\ ( # ` { A } ) = N ) -> N = 1 ) |
15 |
14
|
olcd |
|- ( ( A e. _V /\ ( # ` { A } ) = N ) -> ( N = 0 \/ N = 1 ) ) |
16 |
15
|
ex |
|- ( A e. _V -> ( ( # ` { A } ) = N -> ( N = 0 \/ N = 1 ) ) ) |
17 |
|
snprc |
|- ( -. A e. _V <-> { A } = (/) ) |
18 |
|
fveqeq2 |
|- ( { A } = (/) -> ( ( # ` { A } ) = N <-> ( # ` (/) ) = N ) ) |
19 |
18 8
|
syl6bi |
|- ( { A } = (/) -> ( ( # ` { A } ) = N -> ( N = 0 \/ N = 1 ) ) ) |
20 |
17 19
|
sylbi |
|- ( -. A e. _V -> ( ( # ` { A } ) = N -> ( N = 0 \/ N = 1 ) ) ) |
21 |
16 20
|
pm2.61i |
|- ( ( # ` { A } ) = N -> ( N = 0 \/ N = 1 ) ) |
22 |
10 21
|
syl6bi |
|- ( { x e. { A } | ph } = { A } -> ( ( # ` { x e. { A } | ph } ) = N -> ( N = 0 \/ N = 1 ) ) ) |
23 |
9 22
|
jaoi |
|- ( ( { x e. { A } | ph } = (/) \/ { x e. { A } | ph } = { A } ) -> ( ( # ` { x e. { A } | ph } ) = N -> ( N = 0 \/ N = 1 ) ) ) |
24 |
1 2 23
|
mp2b |
|- ( ( # ` { x e. { A } | ph } ) = N -> ( N = 0 \/ N = 1 ) ) |