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. For a shorter proof requiring ax-un , see epweonALT . (Contributed by NM, 1-Nov-2003) Avoid ax-un . (Revised by BTernaryTau, 30-Nov-2024)

		Ref	Expression
	Assertion	epweon	$⊢ E We On$

Proof

Step	Hyp	Ref	Expression
1		onfr	$⊢ E Fr On$
2		df-po	$⊢ E Po On \leftrightarrow \forall x \in On \forall y \in On \forall z \in On (\neg x E x \land ((x E y \land y E z) \to x E z))$
3		eloni	$⊢ x \in On \to Ord x$
4		ordirr	$⊢ Ord x \to \neg x \in x$
5	3 4	syl	$⊢ x \in On \to \neg x \in x$
6		epel	$⊢ x E x \leftrightarrow x \in x$
7	5 6	sylnibr	$⊢ x \in On \to \neg x E x$
8		ontr1	$⊢ z \in On \to ((x \in y \land y \in z) \to x \in z)$
9		epel	$⊢ x E y \leftrightarrow x \in y$
10		epel	$⊢ y E z \leftrightarrow y \in z$
11	9 10	anbi12i	$⊢ (x E y \land y E z) \leftrightarrow (x \in y \land y \in z)$
12		epel	$⊢ x E z \leftrightarrow x \in z$
13	8 11 12	3imtr4g	$⊢ z \in On \to ((x E y \land y E z) \to x E z)$
14	7 13	anim12i	$⊢ (x \in On \land z \in On) \to (\neg x E x \land ((x E y \land y E z) \to x E z))$
15	14	ralrimiva	$⊢ x \in On \to \forall z \in On (\neg x E x \land ((x E y \land y E z) \to x E z))$
16	15	ralrimivw	$⊢ x \in On \to \forall y \in On \forall z \in On (\neg x E x \land ((x E y \land y E z) \to x E z))$
17	2 16	mprgbir	$⊢ E Po On$
18		eloni	$⊢ y \in On \to Ord y$
19		ordtri3or	$⊢ (Ord x \land Ord y) \to (x \in y \lor x = y \lor y \in x)$
20		biid	$⊢ x = y \leftrightarrow x = y$
21		epel	$⊢ y E x \leftrightarrow y \in x$
22	9 20 21	3orbi123i	$⊢ (x E y \lor x = y \lor y E x) \leftrightarrow (x \in y \lor x = y \lor y \in x)$
23	19 22	sylibr	$⊢ (Ord x \land Ord y) \to (x E y \lor x = y \lor y E x)$
24	3 18 23	syl2an	$⊢ (x \in On \land y \in On) \to (x E y \lor x = y \lor y E x)$
25	24	rgen2	$⊢ \forall x \in On \forall y \in On (x E y \lor x = y \lor y E x)$
26		df-so	$⊢ E Or On \leftrightarrow (E Po On \land \forall x \in On \forall y \in On (x E y \lor x = y \lor y E x))$
27	17 25 26	mpbir2an	$⊢ E Or On$
28		df-we	$⊢ E We On \leftrightarrow (E Fr On \land E Or On)$
29	1 27 28	mpbir2an	$⊢ E We On$

Metamath Proof Explorer

Theorem epweon

Proof