Metamath Proof Explorer

Theorem predon

Description: The predecessor of an ordinal under _E and On is itself. (Contributed by Scott Fenton, 27-Mar-2011) (Proof shortened by BJ, 16-Oct-2024)

Ref Expression
Assertion predon 
|- ( A e. On -> Pred ( _E , On , A ) = A )

Proof

Step Hyp Ref Expression
1 tron 
 |-  Tr On
2 trpred 
 |-  ( ( Tr On /\ A e. On ) -> Pred ( _E , On , A ) = A )
3 1 2 mpan 
 |-  ( A e. On -> Pred ( _E , On , A ) = A )