Metamath Proof Explorer


Theorem hashgt1

Description: Restate "set contains at least two elements" in terms of elementhood. (Contributed by Thierry Arnoux, 21-Nov-2023)

Ref Expression
Assertion hashgt1 A V ¬ A . -1 0 1 1 < A

Proof

Step Hyp Ref Expression
1 hashf . : V 0 +∞
2 ffn . : V 0 +∞ . Fn V
3 elpreima . Fn V A . -1 0 1 A V A 0 1
4 1 2 3 mp2b A . -1 0 1 A V A 0 1
5 elex A V A V
6 5 biantrurd A V A 0 1 A V A 0 1
7 4 6 bitr4id A V A . -1 0 1 A 0 1
8 7 notbid A V ¬ A . -1 0 1 ¬ A 0 1
9 hashxnn0 A V A 0 *
10 xnn01gt A 0 * ¬ A 0 1 1 < A
11 9 10 syl A V ¬ A 0 1 1 < A
12 8 11 bitrd A V ¬ A . -1 0 1 1 < A