Theorem hashgt12el2

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	hashgt12el2	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 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	3ad2ant2	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ( 0 = ( ♯ ‘ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
16	3 15	syl5com	⊢ ( ∅ = 𝑉 → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
17		df-ne	⊢ ( ∅ ≠ 𝑉 ↔ ¬ ∅ = 𝑉 )
18		necom	⊢ ( ∅ ≠ 𝑉 ↔ 𝑉 ≠ ∅ )
19	17 18	bitr3i	⊢ ( ¬ ∅ = 𝑉 ↔ 𝑉 ≠ ∅ )
20		ralnex	⊢ ( ∀ 𝑏 ∈ 𝑉 ¬ 𝐴 ≠ 𝑏 ↔ ¬ ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 )
21		nne	⊢ ( ¬ 𝐴 ≠ 𝑏 ↔ 𝐴 = 𝑏 )
22		eqcom	⊢ ( 𝐴 = 𝑏 ↔ 𝑏 = 𝐴 )
23	21 22	bitri	⊢ ( ¬ 𝐴 ≠ 𝑏 ↔ 𝑏 = 𝐴 )
24	23	ralbii	⊢ ( ∀ 𝑏 ∈ 𝑉 ¬ 𝐴 ≠ 𝑏 ↔ ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 )
25	20 24	bitr3i	⊢ ( ¬ ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ↔ ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 )
26		eqsn	⊢ ( 𝑉 ≠ ∅ → ( 𝑉 = { 𝐴 } ↔ ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 ) )
27	26	bicomd	⊢ ( 𝑉 ≠ ∅ → ( ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = { 𝐴 } ) )
28	27	adantl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = { 𝐴 } ) )
29	28	adantr	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = { 𝐴 } ) )
30		hashsnle1	⊢ ( ♯ ‘ { 𝐴 } ) ≤ 1
31		fveq2	⊢ ( 𝑉 = { 𝐴 } → ( ♯ ‘ 𝑉 ) = ( ♯ ‘ { 𝐴 } ) )
32	31	breq1d	⊢ ( 𝑉 = { 𝐴 } → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ( ♯ ‘ { 𝐴 } ) ≤ 1 ) )
33	32	adantl	⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑉 = { 𝐴 } ) → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ( ♯ ‘ { 𝐴 } ) ≤ 1 ) )
34	30 33	mpbiri	⊢ ( ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) ∧ 𝑉 = { 𝐴 } ) → ( ♯ ‘ 𝑉 ) ≤ 1 )
35	34	ex	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑉 = { 𝐴 } → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
36	29 35	sylbid	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 → ( ♯ ‘ 𝑉 ) ≤ 1 ) )
37		hashxrcl	⊢ ( 𝑉 ∈ 𝑊 → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
38	37	adantr	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
39	38	adantr	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ♯ ‘ 𝑉 ) ∈ ℝ* )
40		1xr	⊢ 1 ∈ ℝ*
41		xrlenlt	⊢ ( ( ( ♯ ‘ 𝑉 ) ∈ ℝ* ∧ 1 ∈ ℝ* ) → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
42	39 40 41	sylancl	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ( ♯ ‘ 𝑉 ) ≤ 1 ↔ ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
43	36 42	sylibd	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ∀ 𝑏 ∈ 𝑉 𝑏 = 𝐴 → ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
44	25 43	syl5bi	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( ¬ ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 → ¬ 1 < ( ♯ ‘ 𝑉 ) ) )
45	44	con4d	⊢ ( ( ( 𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅ ) ∧ 𝐴 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
46	45	exp31	⊢ ( 𝑉 ∈ 𝑊 → ( 𝑉 ≠ ∅ → ( 𝐴 ∈ 𝑉 → ( 1 < ( ♯ ‘ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) ) ) )
47	46	com24	⊢ ( 𝑉 ∈ 𝑊 → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐴 ∈ 𝑉 → ( 𝑉 ≠ ∅ → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) ) ) )
48	47	3imp	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ( 𝑉 ≠ ∅ → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
49	48	com12	⊢ ( 𝑉 ≠ ∅ → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
50	19 49	sylbi	⊢ ( ¬ ∅ = 𝑉 → ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ) )
51	16 50	pm2.61i	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝐴 ∈ 𝑉 ) → ∃ 𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 )