Theorem 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	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 )

Proof

Step	Hyp	Ref	Expression
1		hash0	⊢ ( ♯ ‘ ∅ ) = 0
2		fveq2	⊢ ( ∅ = 𝑉 → ( ♯ ‘ ∅ ) = ( ♯ ‘ 𝑉 ) )
3	1 2	eqtr3id	⊢ ( ∅ = 𝑉 → 0 = ( ♯ ‘ 𝑉 ) )
4		breq2	⊢ ( ( ♯ ‘ 𝑉 ) = 0 → ( 1 < ( ♯ ‘ 𝑉 ) ↔ 1 < 0 ) )
5	4	biimpd	⊢ ( ( ♯ ‘ 𝑉 ) = 0 → ( 1 < ( ♯ ‘ 𝑉 ) → 1 < 0 ) )
6	5	eqcoms	⊢ ( 0 = ( ♯ ‘ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → 1 < 0 ) )
7		0le1	⊢ 0 ≤ 1
8		0re	⊢ 0 ∈ ℝ
9		1re	⊢ 1 ∈ ℝ
10	8 9	lenlti	⊢ ( 0 ≤ 1 ↔ ¬ 1 < 0 )
11		pm2.21	⊢ ( ¬ 1 < 0 → ( 1 < 0 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
12	10 11	sylbi	⊢ ( 0 ≤ 1 → ( 1 < 0 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
13	7 12	ax-mp	⊢ ( 1 < 0 → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 )
14	6 13	syl6com	⊢ ( 1 < ( ♯ ‘ 𝑉 ) → ( 0 = ( ♯ ‘ 𝑉 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
15	14	adantl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( 0 = ( ♯ ‘ 𝑉 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
16	15	com12	⊢ ( 0 = ( ♯ ‘ 𝑉 ) → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
17	3 16	syl	⊢ ( ∅ = 𝑉 → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
18		df-ne	⊢ ( ∅ ≠ 𝑉 ↔ ¬ ∅ = 𝑉 )
19		necom	⊢ ( ∅ ≠ 𝑉 ↔ 𝑉 ≠ ∅ )
20	18 19	bitr3i	⊢ ( ¬ ∅ = 𝑉 ↔ 𝑉 ≠ ∅ )
21		ralnex	⊢ ( ∀ 𝑎 ∈ 𝑉 ¬ ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ↔ ¬ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 )
22		ralnex	⊢ ( ∀ 𝑏 ∈ 𝑉 ¬ 𝑎 ≠ 𝑏 ↔ ¬ ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 )
23		nne	⊢ ( ¬ 𝑎 ≠ 𝑏 ↔ 𝑎 = 𝑏 )
24		equcom	⊢ ( 𝑎 = 𝑏 ↔ 𝑏 = 𝑎 )
25	23 24	bitri	⊢ ( ¬ 𝑎 ≠ 𝑏 ↔ 𝑏 = 𝑎 )
26	25	ralbii	⊢ ( ∀ 𝑏 ∈ 𝑉 ¬ 𝑎 ≠ 𝑏 ↔ ∀ 𝑏 ∈ 𝑉 𝑏 = 𝑎 )
27	22 26	bitr3i	⊢ ( ¬ ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ↔ ∀ 𝑏 ∈ 𝑉 𝑏 = 𝑎 )
28	27	ralbii	⊢ ( ∀ 𝑎 ∈ 𝑉 ¬ ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 𝑏 = 𝑎 )
29	21 28	bitr3i	⊢ ( ¬ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ↔ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 𝑏 = 𝑎 )
30		eqsn	⊢ ( 𝑉 ≠ ∅ → ( 𝑉 = { 𝑎 } ↔ ∀ 𝑏 ∈ 𝑉 𝑏 = 𝑎 ) )
31	30	adantl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( 𝑉 = { 𝑎 } ↔ ∀ 𝑏 ∈ 𝑉 𝑏 = 𝑎 ) )
32	31	bicomd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑏 ∈ 𝑉 𝑏 = 𝑎 ↔ 𝑉 = { 𝑎 } ) )
33	32	ralbidv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 𝑏 = 𝑎 ↔ ∀ 𝑎 ∈ 𝑉 𝑉 = { 𝑎 } ) )
34		fveq2	⊢ ( 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ { 𝑎 } ) )
35		hashsnle1	⊢ ( ♯ ‘ { 𝑎 } ) ≤ 1
36	34 35	eqbrtrdi	⊢ ( 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 )
37	36	a1i	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑎 ∈ 𝑉 ) → ( 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
38	37	reximdva0	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ∃ 𝑎 ∈ 𝑉 ( 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
39		r19.36v	⊢ ( ∃ 𝑎 ∈ 𝑉 ( 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) → ( ∀ 𝑎 ∈ 𝑉 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
40	38 39	syl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑎 ∈ 𝑉 𝑉 = { 𝑎 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
41	33 40	sylbid	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 𝑏 = 𝑎 → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
42		hashxrcl	⊢ ( 𝑉 ∈ 𝑊 → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
43	42	adantr	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
44		1xr	⊢ 1 ∈ ℝ*
45		xrlenlt	⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
46	43 44 45	sylancl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
47	41 46	sylibd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 𝑏 = 𝑎 → ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
48	29 47	syl5bi	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ¬ ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 → ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
49	48	con4d	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( 1 < ( ♯ ‘ 𝑉 ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
50	49	impancom	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( 𝑉 ≠ ∅ → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
51	50	com12	⊢ ( 𝑉 ≠ ∅ → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
52	20 51	sylbi	⊢ ( ¬ ∅ = 𝑉 → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 ) )
53	17 52	pm2.61i	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∃ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 𝑎 ≠ 𝑏 )