Description: Alternate proof of onprc from onprcr . (Contributed by Adrian Ducourtial, 15-Oct-2026) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | onprcALT | |- -. On e. _V |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-on | |- On = { x | Ord x } |
|
| 2 | rabab | |- { x e. _V | Ord x } = { x | Ord x } |
|
| 3 | 1 2 | eqtr4i | |- On = { x e. _V | Ord x } |
| 4 | tron | |- Tr On |
|
| 5 | 3 4 | onprcr | |- -. On e. _V |