Theorem on0eqel

Description: An ordinal number either equals zero or contains zero. (Contributed by NM, 1-Jun-2004)

	Ref	Expression
Assertion	on0eqel	$$⊢A\in \mathrm{On}\to \left(A=\varnothing \vee \varnothing \in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq A$$
2		0elon	$$⊢\varnothing \in \mathrm{On}$$
3		onsseleq	$$⊢\left(\varnothing \in \mathrm{On}\wedge A\in \mathrm{On}\right)\to \left(\varnothing \subseteq A\leftrightarrow \left(\varnothing \in A\vee \varnothing =A\right)\right)$$
4	2 3	mpan	$$⊢A\in \mathrm{On}\to \left(\varnothing \subseteq A\leftrightarrow \left(\varnothing \in A\vee \varnothing =A\right)\right)$$
5	1 4	mpbii	$$⊢A\in \mathrm{On}\to \left(\varnothing \in A\vee \varnothing =A\right)$$
6		eqcom	$$⊢\varnothing =A\leftrightarrow A=\varnothing$$
7	6	orbi2i	$$⊢\left(\varnothing \in A\vee \varnothing =A\right)\leftrightarrow \left(\varnothing \in A\vee A=\varnothing \right)$$
8		orcom	$$⊢\left(\varnothing \in A\vee A=\varnothing \right)\leftrightarrow \left(A=\varnothing \vee \varnothing \in A\right)$$
9	7 8	bitri	$$⊢\left(\varnothing \in A\vee \varnothing =A\right)\leftrightarrow \left(A=\varnothing \vee \varnothing \in A\right)$$
10	5 9	sylib	$$⊢A\in \mathrm{On}\to \left(A=\varnothing \vee \varnothing \in A\right)$$