Theorem on0eqel

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

	Ref	Expression
Assertion	on0eqel	|- ( A e. On -> ( A = (/) \/ (/) e. A ) )

Proof

Step	Hyp	Ref	Expression
1		0ss	|- (/) C_ A
2		0elon	|- (/) e. On
3		onsseleq	|- ( ( (/) e. On /\ A e. On ) -> ( (/) C_ A <-> ( (/) e. A \/ (/) = A ) ) )
4	2 3	mpan	|- ( A e. On -> ( (/) C_ A <-> ( (/) e. A \/ (/) = A ) ) )
5	1 4	mpbii	|- ( A e. On -> ( (/) e. A \/ (/) = A ) )
6		eqcom	|- ( (/) = A <-> A = (/) )
7	6	orbi2i	|- ( ( (/) e. A \/ (/) = A ) <-> ( (/) e. A \/ A = (/) ) )
8		orcom	|- ( ( (/) e. A \/ A = (/) ) <-> ( A = (/) \/ (/) e. A ) )
9	7 8	bitri	|- ( ( (/) e. A \/ (/) = A ) <-> ( A = (/) \/ (/) e. A ) )
10	5 9	sylib	|- ( A e. On -> ( A = (/) \/ (/) e. A ) )