Description: Less-than class is never reflexive. (Contributed by Ender Ting, 22-Nov-2024) Prefer to specify theorem domain and then apply ltnri . (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | et-ltneverrefl | |- -. A < A |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | xrltnr | |- ( A e. RR* -> -. A < A ) |
|
| 2 | opelxp1 | |- ( <. A , A >. e. ( RR* X. RR* ) -> A e. RR* ) |
|
| 3 | 2 | con3i | |- ( -. A e. RR* -> -. <. A , A >. e. ( RR* X. RR* ) ) |
| 4 | ltrelxr | |- < C_ ( RR* X. RR* ) |
|
| 5 | 4 | sseli | |- ( <. A , A >. e. < -> <. A , A >. e. ( RR* X. RR* ) ) |
| 6 | 3 5 | nsyl | |- ( -. A e. RR* -> -. <. A , A >. e. < ) |
| 7 | df-br | |- ( A < A <-> <. A , A >. e. < ) |
|
| 8 | 6 7 | sylnibr | |- ( -. A e. RR* -> -. A < A ) |
| 9 | 1 8 | pm2.61i | |- -. A < A |