Metamath Proof Explorer

Theorem epweonALT

Description: Alternate proof of epweon , shorter but requiring ax-un . (Contributed by NM, 1-Nov-2003) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	epweonALT	$⊢ E We On$

Proof

Step	Hyp	Ref	Expression
1		onfr	$⊢ E Fr On$
2		eloni	$⊢ x \in On \to Ord x$
3		eloni	$⊢ y \in On \to Ord y$
4		ordtri3or	$⊢ (Ord x \land Ord y) \to (x \in y \lor x = y \lor y \in x)$
5		epel	$⊢ x E y \leftrightarrow x \in y$
6		biid	$⊢ x = y \leftrightarrow x = y$
7		epel	$⊢ y E x \leftrightarrow y \in x$
8	5 6 7	3orbi123i	$⊢ (x E y \lor x = y \lor y E x) \leftrightarrow (x \in y \lor x = y \lor y \in x)$
9	4 8	sylibr	$⊢ (Ord x \land Ord y) \to (x E y \lor x = y \lor y E x)$
10	2 3 9	syl2an	$⊢ (x \in On \land y \in On) \to (x E y \lor x = y \lor y E x)$
11	10	rgen2	$⊢ \forall x \in On \forall y \in On (x E y \lor x = y \lor y E x)$
12		dfwe2	$⊢ E We On \leftrightarrow (E Fr On \land \forall x \in On \forall y \in On (x E y \lor x = y \lor y E x))$
13	1 11 12	mpbir2an	$⊢ E We On$