Metamath Proof Explorer

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 ⊢V∈W∧1<V∧A∈V→∃b∈VA≠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∈ℝ
9 1re ⊢1∈ℝ
10 8 9 lenlti ⊢0≤1↔¬1<0
11 pm2.21 ⊢¬1<0→1<0→∃b∈VA≠b
12 10 11 sylbi ⊢0≤1→1<0→∃b∈VA≠b
13 7 12 ax-mp ⊢1<0→∃b∈VA≠b
14 6 13 syl6com ⊢1<V→0=V→∃b∈VA≠b
15 14 3ad2ant2 ⊢V∈W∧1<V∧A∈V→0=V→∃b∈VA≠b
16 3 15 syl5com ⊢∅=V→V∈W∧1<V∧A∈V→∃b∈VA≠b
17 df-ne ⊢∅≠V↔¬∅=V
18 necom ⊢∅≠V↔V≠∅
19 17 18 bitr3i ⊢¬∅=V↔V≠∅
20 ralnex ⊢∀b∈V¬A≠b↔¬∃b∈VA≠b
21 nne ⊢¬A≠b↔A=b
22 eqcom ⊢A=b↔b=A
23 21 22 bitri ⊢¬A≠b↔b=A
24 23 ralbii ⊢∀b∈V¬A≠b↔∀b∈Vb=A
25 20 24 bitr3i ⊢¬∃b∈VA≠b↔∀b∈Vb=A
26 eqsn ⊢V≠∅→V=A↔∀b∈Vb=A
27 26 bicomd ⊢V≠∅→∀b∈Vb=A↔V=A
28 27 adantl ⊢V∈W∧V≠∅→∀b∈Vb=A↔V=A
29 28 adantr ⊢V∈W∧V≠∅∧A∈V→∀b∈Vb=A↔V=A
30 hashsnle1 ⊢A≤1
31 fveq2 ⊢V=A→V=A
32 31 breq1d ⊢V=A→V≤1↔A≤1
33 32 adantl ⊢V∈W∧V≠∅∧A∈V∧V=A→V≤1↔A≤1
34 30 33 mpbiri ⊢V∈W∧V≠∅∧A∈V∧V=A→V≤1
35 34 ex ⊢V∈W∧V≠∅∧A∈V→V=A→V≤1
36 29 35 sylbid ⊢V∈W∧V≠∅∧A∈V→∀b∈Vb=A→V≤1
37 hashxrcl ⊢V∈W→V∈ℝ*
38 37 adantr ⊢V∈W∧V≠∅→V∈ℝ*
39 38 adantr ⊢V∈W∧V≠∅∧A∈V→V∈ℝ*
40 1xr ⊢1∈ℝ*
41 xrlenlt ⊢V∈ℝ*∧1∈ℝ*→V≤1↔¬1<V
42 39 40 41 sylancl ⊢V∈W∧V≠∅∧A∈V→V≤1↔¬1<V
43 36 42 sylibd ⊢V∈W∧V≠∅∧A∈V→∀b∈Vb=A→¬1<V
44 25 43 biimtrid ⊢V∈W∧V≠∅∧A∈V→¬∃b∈VA≠b→¬1<V
45 44 con4d ⊢V∈W∧V≠∅∧A∈V→1<V→∃b∈VA≠b
46 45 exp31 ⊢V∈W→V≠∅→A∈V→1<V→∃b∈VA≠b
47 46 com24 ⊢V∈W→1<V→A∈V→V≠∅→∃b∈VA≠b
48 47 3imp ⊢V∈W∧1<V∧A∈V→V≠∅→∃b∈VA≠b
49 48 com12 ⊢V≠∅→V∈W∧1<V∧A∈V→∃b∈VA≠b
50 19 49 sylbi ⊢¬∅=V→V∈W∧1<V∧A∈V→∃b∈VA≠b
51 16 50 pm2.61i ⊢V∈W∧1<V∧A∈V→∃b∈VA≠b