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 ∈ On → Ord ⁡ x
3 eloni ⊢ y ∈ On → Ord ⁡ y
4 ordtri3or ⊢ Ord ⁡ x ∧ Ord ⁡ y → x ∈ y ∨ x = y ∨ y ∈ x
5 epel ⊢ x E y ↔ x ∈ y
6 biid ⊢ x = y ↔ x = y
7 epel ⊢ y E x ↔ y ∈ x
8 5 6 7 3orbi123i ⊢ x E y ∨ x = y ∨ y E x ↔ x ∈ y ∨ x = y ∨ y ∈ x
9 4 8 sylibr ⊢ Ord ⁡ x ∧ Ord ⁡ y → x E y ∨ x = y ∨ y E x
10 2 3 9 syl2an ⊢ x ∈ On ∧ y ∈ On → x E y ∨ x = y ∨ y E x
11 10 rgen2 ⊢ ∀ x ∈ On ∀ y ∈ On x E y ∨ x = y ∨ y E x
12 dfwe2 ⊢ E We On ↔ E Fr On ∧ ∀ x ∈ On ∀ y ∈ On x E y ∨ x = y ∨ y E x
13 1 11 12 mpbir2an ⊢ E We On