Metamath Proof Explorer

Theorem epirron

Description: The strict order on the ordinals is irreflexive. Theorem 1.9(i) of Schloeder p. 1. (Contributed by RP, 15-Jan-2025)

Ref Expression
Assertion epirron 
|- ( A e. On -> -. A _E A )

Proof

Step Hyp Ref Expression
1 epweon 
 |-  _E We On
2 weso 
 |-  ( _E We On -> _E Or On )
3 sopo 
 |-  ( _E Or On -> _E Po On )
4 1 2 3 mp2b 
 |-  _E Po On
5 poirr 
 |-  ( ( _E Po On /\ A e. On ) -> -. A _E A )
6 4 5 mpan 
 |-  ( A e. On -> -. A _E A )