Description: Any set dominates the empty set. (Contributed by NM, 26-Oct-2003) (Revised by Mario Carneiro, 26-Apr-2015) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0domg | |- ( A e. V -> (/) ~<_ A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0ex | |- (/) e. _V |
|
| 2 | f1eq1 | |- ( f = (/) -> ( f : (/) -1-1-> A <-> (/) : (/) -1-1-> A ) ) |
|
| 3 | f10 | |- (/) : (/) -1-1-> A |
|
| 4 | 1 2 3 | ceqsexv2d | |- E. f f : (/) -1-1-> A |
| 5 | brdom2g | |- ( ( (/) e. _V /\ A e. V ) -> ( (/) ~<_ A <-> E. f f : (/) -1-1-> A ) ) |
|
| 6 | 1 5 | mpan | |- ( A e. V -> ( (/) ~<_ A <-> E. f f : (/) -1-1-> A ) ) |
| 7 | 4 6 | mpbiri | |- ( A e. V -> (/) ~<_ A ) |