Theorem epweon

Description: The membership relation well-orders the class of ordinal numbers. This proof does not require the axiom of regularity. Proposition 4.8(g) of Mendelson p. 244. (Contributed by NM, 1-Nov-2003)

	Ref	Expression
Assertion	epweon	⊢ E We On

Proof

Step	Hyp	Ref	Expression
1		onfr	⊢ E Fr On
2		eloni	⊢ ( 𝑥 ∈ On → Ord 𝑥 )
3		eloni	⊢ ( 𝑦 ∈ On → Ord 𝑦 )
4		ordtri3or	⊢ ( ( Ord 𝑥 ∧ Ord 𝑦 ) → ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) )
5		epel	⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
6		biid	⊢ ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑦 )
7		epel	⊢ ( 𝑦 E 𝑥 ↔ 𝑦 ∈ 𝑥 )
8	5 6 7	3orbi123i	⊢ ( ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥 ) )
9	4 8	sylibr	⊢ ( ( Ord 𝑥 ∧ Ord 𝑦 ) → ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) )
10	2 3 9	syl2an	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) → ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) )
11	10	rgen2	⊢ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 )
12		dfwe2	⊢ ( E We On ↔ ( E Fr On ∧ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( 𝑥 E 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 E 𝑥 ) ) )
13	1 11 12	mpbir2an	⊢ E We On