Description: Alternate proof of dju1p1e2 . (Contributed by Mario Carneiro, 29-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | dju1p1e2ALT | |- ( 1o |_| 1o ) ~~ 2o |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 1on | |- 1o e. On |
|
| 2 | 1 | onordi | |- Ord 1o |
| 3 | ordirr | |- ( Ord 1o -> -. 1o e. 1o ) |
|
| 4 | 2 3 | ax-mp | |- -. 1o e. 1o |
| 5 | dju1en | |- ( ( 1o e. On /\ -. 1o e. 1o ) -> ( 1o |_| 1o ) ~~ suc 1o ) |
|
| 6 | 1 4 5 | mp2an | |- ( 1o |_| 1o ) ~~ suc 1o |
| 7 | df-2o | |- 2o = suc 1o |
|
| 8 | 6 7 | breqtrri | |- ( 1o |_| 1o ) ~~ 2o |