This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑥 ∈ 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