Step |
Hyp |
Ref |
Expression |
1 |
|
hash0 |
|- ( # ` (/) ) = 0 |
2 |
|
fveq2 |
|- ( (/) = V -> ( # ` (/) ) = ( # ` V ) ) |
3 |
1 2
|
eqtr3id |
|- ( (/) = V -> 0 = ( # ` V ) ) |
4 |
|
breq2 |
|- ( ( # ` V ) = 0 -> ( 1 < ( # ` V ) <-> 1 < 0 ) ) |
5 |
4
|
biimpd |
|- ( ( # ` V ) = 0 -> ( 1 < ( # ` V ) -> 1 < 0 ) ) |
6 |
5
|
eqcoms |
|- ( 0 = ( # ` V ) -> ( 1 < ( # ` V ) -> 1 < 0 ) ) |
7 |
|
0le1 |
|- 0 <_ 1 |
8 |
|
0re |
|- 0 e. RR |
9 |
|
1re |
|- 1 e. RR |
10 |
8 9
|
lenlti |
|- ( 0 <_ 1 <-> -. 1 < 0 ) |
11 |
|
pm2.21 |
|- ( -. 1 < 0 -> ( 1 < 0 -> E. a e. V E. b e. V a =/= b ) ) |
12 |
10 11
|
sylbi |
|- ( 0 <_ 1 -> ( 1 < 0 -> E. a e. V E. b e. V a =/= b ) ) |
13 |
7 12
|
ax-mp |
|- ( 1 < 0 -> E. a e. V E. b e. V a =/= b ) |
14 |
6 13
|
syl6com |
|- ( 1 < ( # ` V ) -> ( 0 = ( # ` V ) -> E. a e. V E. b e. V a =/= b ) ) |
15 |
14
|
adantl |
|- ( ( V e. W /\ 1 < ( # ` V ) ) -> ( 0 = ( # ` V ) -> E. a e. V E. b e. V a =/= b ) ) |
16 |
15
|
com12 |
|- ( 0 = ( # ` V ) -> ( ( V e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. V a =/= b ) ) |
17 |
3 16
|
syl |
|- ( (/) = V -> ( ( V e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. V a =/= b ) ) |
18 |
|
df-ne |
|- ( (/) =/= V <-> -. (/) = V ) |
19 |
|
necom |
|- ( (/) =/= V <-> V =/= (/) ) |
20 |
18 19
|
bitr3i |
|- ( -. (/) = V <-> V =/= (/) ) |
21 |
|
ralnex |
|- ( A. a e. V -. E. b e. V a =/= b <-> -. E. a e. V E. b e. V a =/= b ) |
22 |
|
ralnex |
|- ( A. b e. V -. a =/= b <-> -. E. b e. V a =/= b ) |
23 |
|
nne |
|- ( -. a =/= b <-> a = b ) |
24 |
|
equcom |
|- ( a = b <-> b = a ) |
25 |
23 24
|
bitri |
|- ( -. a =/= b <-> b = a ) |
26 |
25
|
ralbii |
|- ( A. b e. V -. a =/= b <-> A. b e. V b = a ) |
27 |
22 26
|
bitr3i |
|- ( -. E. b e. V a =/= b <-> A. b e. V b = a ) |
28 |
27
|
ralbii |
|- ( A. a e. V -. E. b e. V a =/= b <-> A. a e. V A. b e. V b = a ) |
29 |
21 28
|
bitr3i |
|- ( -. E. a e. V E. b e. V a =/= b <-> A. a e. V A. b e. V b = a ) |
30 |
|
eqsn |
|- ( V =/= (/) -> ( V = { a } <-> A. b e. V b = a ) ) |
31 |
30
|
adantl |
|- ( ( V e. W /\ V =/= (/) ) -> ( V = { a } <-> A. b e. V b = a ) ) |
32 |
31
|
bicomd |
|- ( ( V e. W /\ V =/= (/) ) -> ( A. b e. V b = a <-> V = { a } ) ) |
33 |
32
|
ralbidv |
|- ( ( V e. W /\ V =/= (/) ) -> ( A. a e. V A. b e. V b = a <-> A. a e. V V = { a } ) ) |
34 |
|
fveq2 |
|- ( V = { a } -> ( # ` V ) = ( # ` { a } ) ) |
35 |
|
hashsnle1 |
|- ( # ` { a } ) <_ 1 |
36 |
34 35
|
eqbrtrdi |
|- ( V = { a } -> ( # ` V ) <_ 1 ) |
37 |
36
|
a1i |
|- ( ( V e. W /\ a e. V ) -> ( V = { a } -> ( # ` V ) <_ 1 ) ) |
38 |
37
|
reximdva0 |
|- ( ( V e. W /\ V =/= (/) ) -> E. a e. V ( V = { a } -> ( # ` V ) <_ 1 ) ) |
39 |
|
r19.36v |
|- ( E. a e. V ( V = { a } -> ( # ` V ) <_ 1 ) -> ( A. a e. V V = { a } -> ( # ` V ) <_ 1 ) ) |
40 |
38 39
|
syl |
|- ( ( V e. W /\ V =/= (/) ) -> ( A. a e. V V = { a } -> ( # ` V ) <_ 1 ) ) |
41 |
33 40
|
sylbid |
|- ( ( V e. W /\ V =/= (/) ) -> ( A. a e. V A. b e. V b = a -> ( # ` V ) <_ 1 ) ) |
42 |
|
hashxrcl |
|- ( V e. W -> ( # ` V ) e. RR* ) |
43 |
42
|
adantr |
|- ( ( V e. W /\ V =/= (/) ) -> ( # ` V ) e. RR* ) |
44 |
|
1xr |
|- 1 e. RR* |
45 |
|
xrlenlt |
|- ( ( ( # ` V ) e. RR* /\ 1 e. RR* ) -> ( ( # ` V ) <_ 1 <-> -. 1 < ( # ` V ) ) ) |
46 |
43 44 45
|
sylancl |
|- ( ( V e. W /\ V =/= (/) ) -> ( ( # ` V ) <_ 1 <-> -. 1 < ( # ` V ) ) ) |
47 |
41 46
|
sylibd |
|- ( ( V e. W /\ V =/= (/) ) -> ( A. a e. V A. b e. V b = a -> -. 1 < ( # ` V ) ) ) |
48 |
29 47
|
syl5bi |
|- ( ( V e. W /\ V =/= (/) ) -> ( -. E. a e. V E. b e. V a =/= b -> -. 1 < ( # ` V ) ) ) |
49 |
48
|
con4d |
|- ( ( V e. W /\ V =/= (/) ) -> ( 1 < ( # ` V ) -> E. a e. V E. b e. V a =/= b ) ) |
50 |
49
|
impancom |
|- ( ( V e. W /\ 1 < ( # ` V ) ) -> ( V =/= (/) -> E. a e. V E. b e. V a =/= b ) ) |
51 |
50
|
com12 |
|- ( V =/= (/) -> ( ( V e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. V a =/= b ) ) |
52 |
20 51
|
sylbi |
|- ( -. (/) = V -> ( ( V e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. V a =/= b ) ) |
53 |
17 52
|
pm2.61i |
|- ( ( V e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. V a =/= b ) |