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