This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dom0

Description: A set dominated by the empty set is empty. (Contributed by NM, 22-Nov-2004) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)

Ref Expression
Assertion dom0 
|- ( A ~<_ (/) <-> A = (/) )

Proof

Step Hyp Ref Expression
1 brdomi 
 |-  ( A ~<_ (/) -> E. f f : A -1-1-> (/) )
2 f1f 
 |-  ( f : A -1-1-> (/) -> f : A --> (/) )
3 f00 
 |-  ( f : A --> (/) <-> ( f = (/) /\ A = (/) ) )
4 3 simprbi 
 |-  ( f : A --> (/) -> A = (/) )
5 2 4 syl 
 |-  ( f : A -1-1-> (/) -> A = (/) )
6 5 exlimiv 
 |-  ( E. f f : A -1-1-> (/) -> A = (/) )
7 1 6 syl 
 |-  ( A ~<_ (/) -> A = (/) )
8 en0 
 |-  ( A ~~ (/) <-> A = (/) )
9 endom 
 |-  ( A ~~ (/) -> A ~<_ (/) )
10 8 9 sylbir 
 |-  ( A = (/) -> A ~<_ (/) )
11 7 10 impbii 
 |-  ( A ~<_ (/) <-> A = (/) )