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	$$⊢\left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx 2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
2	1	onordi	$$⊢\mathrm{Ord}{1}_{𝑜}$$
3		ordirr	$$⊢\mathrm{Ord}{1}_{𝑜}\to \neg 1_{𝑜}\in 1_{𝑜}$$
4	2 3	ax-mp	$$⊢\neg 1_{𝑜}\in 1_{𝑜}$$
5		dju1en	$$⊢\left(1_{𝑜}\in \mathrm{On}\wedge \neg 1_{𝑜}\in 1_{𝑜}\right)\to \left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx \mathrm{suc}{1}_{𝑜}$$
6	1 4 5	mp2an	$$⊢\left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx \mathrm{suc}{1}_{𝑜}$$
7		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
8	6 7	breqtrri	$$⊢\left(1_{𝑜}\mathrm{\bigsqcup ︀}{1}_{𝑜}\right)\approx 2_{𝑜}$$