Description: The empty set does not strictly dominate any set. (Contributed by NM, 26-Oct-2003) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 29-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sdom0 | |- -. A ~< (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dom0 | |- ( A ~<_ (/) <-> A = (/) ) |
|
| 2 | en0 | |- ( A ~~ (/) <-> A = (/) ) |
|
| 3 | 1 2 | sylbb2 | |- ( A ~<_ (/) -> A ~~ (/) ) |
| 4 | iman | |- ( ( A ~<_ (/) -> A ~~ (/) ) <-> -. ( A ~<_ (/) /\ -. A ~~ (/) ) ) |
|
| 5 | 3 4 | mpbi | |- -. ( A ~<_ (/) /\ -. A ~~ (/) ) |
| 6 | brsdom | |- ( A ~< (/) <-> ( A ~<_ (/) /\ -. A ~~ (/) ) ) |
|
| 7 | 5 6 | mtbir | |- -. A ~< (/) |