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	⊢ ( 𝐴 ∈ On → ¬ 𝐴 E 𝐴 )

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 ∧ 𝐴 ∈ On ) → ¬ 𝐴 E 𝐴 )
6	4 5	mpan	⊢ ( 𝐴 ∈ On → ¬ 𝐴 E 𝐴 )