hashgt12el

Description: In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017)

		Ref	Expression
	Assertion	hashgt12el	\|- ( ( V e. W /\ 1 < ( # ` V ) ) -> E. a e. V E. b e. V a =/= b )

Proof

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	biimtrid	\|- ( ( 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 )

Metamath Proof Explorer

Theorem hashgt12el

Proof