Description: Obsolete version of sdom0 as of 29-Nov-2024. (Contributed by NM, 26-Oct-2003) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sdom0OLD | |- -. A ~< (/) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relsdom | |- Rel ~< |
|
| 2 | 1 | brrelex1i | |- ( A ~< (/) -> A e. _V ) |
| 3 | 0domg | |- ( A e. _V -> (/) ~<_ A ) |
|
| 4 | 2 3 | syl | |- ( A ~< (/) -> (/) ~<_ A ) |
| 5 | domnsym | |- ( (/) ~<_ A -> -. A ~< (/) ) |
|
| 6 | 5 | con2i | |- ( A ~< (/) -> -. (/) ~<_ A ) |
| 7 | 4 6 | pm2.65i | |- -. A ~< (/) |