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

Metamath Proof Explorer

Theorem dju1p1e2ALT

Description: Alternate proof of dju1p1e2 . (Contributed by Mario Carneiro, 29-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dju1p1e2ALT ( 1o ⊔ 1o ) ≈ 2o

Proof

Step Hyp Ref Expression
1 1on ⊢ 1o ∈ On
2 1 onordi ⊢ Ord 1o
3 ordirr ⊢ ( Ord 1o → ¬ 1o ∈ 1o )
4 2 3 ax-mp ⊢ ¬ 1o ∈ 1o
5 dju1en ⊢ ( ( 1o ∈ On ∧ ¬ 1o ∈ 1o ) → ( 1o ⊔ 1o ) ≈ suc 1o )
6 1 4 5 mp2an ⊢ ( 1o ⊔ 1o ) ≈ suc 1o
7 df-2o ⊢ 2o = suc 1o
8 6 7 breqtrri ⊢ ( 1o ⊔ 1o ) ≈ 2o