Metamath Proof Explorer


Theorem hashneq0

Description: Two ways of saying a set is not empty. (Contributed by Alexander van der Vekens, 23-Sep-2018)

Ref Expression
Assertion hashneq0 A V 0 < A A

Proof

Step Hyp Ref Expression
1 hashnn0pnf A V A 0 A = +∞
2 nn0re A 0 A
3 nn0ge0 A 0 0 A
4 ne0gt0 A 0 A A 0 0 < A
5 2 3 4 syl2anc A 0 A 0 0 < A
6 5 bicomd A 0 0 < A A 0
7 breq2 A = +∞ 0 < A 0 < +∞
8 0ltpnf 0 < +∞
9 0re 0
10 renepnf 0 0 +∞
11 9 10 ax-mp 0 +∞
12 11 necomi +∞ 0
13 8 12 2th 0 < +∞ +∞ 0
14 neeq1 A = +∞ A 0 +∞ 0
15 13 14 bitr4id A = +∞ 0 < +∞ A 0
16 7 15 bitrd A = +∞ 0 < A A 0
17 6 16 jaoi A 0 A = +∞ 0 < A A 0
18 1 17 syl A V 0 < A A 0
19 hasheq0 A V A = 0 A =
20 19 necon3bid A V A 0 A
21 18 20 bitrd A V 0 < A A