Theorem on0eqel

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

	Ref	Expression
Assertion	on0eqel	⊢ ( 𝐴 ∈ On → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ 𝐴
2		0elon	⊢ ∅ ∈ On
3		onsseleq	⊢ ( ( ∅ ∈ On ∧ 𝐴 ∈ On ) → ( ∅ ⊆ 𝐴 ↔ ( ∅ ∈ 𝐴 ∨ ∅ = 𝐴 ) ) )
4	2 3	mpan	⊢ ( 𝐴 ∈ On → ( ∅ ⊆ 𝐴 ↔ ( ∅ ∈ 𝐴 ∨ ∅ = 𝐴 ) ) )
5	1 4	mpbii	⊢ ( 𝐴 ∈ On → ( ∅ ∈ 𝐴 ∨ ∅ = 𝐴 ) )
6		eqcom	⊢ ( ∅ = 𝐴 ↔ 𝐴 = ∅ )
7	6	orbi2i	⊢ ( ( ∅ ∈ 𝐴 ∨ ∅ = 𝐴 ) ↔ ( ∅ ∈ 𝐴 ∨ 𝐴 = ∅ ) )
8		orcom	⊢ ( ( ∅ ∈ 𝐴 ∨ 𝐴 = ∅ ) ↔ ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
9	7 8	bitri	⊢ ( ( ∅ ∈ 𝐴 ∨ ∅ = 𝐴 ) ↔ ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )
10	5 9	sylib	⊢ ( 𝐴 ∈ On → ( 𝐴 = ∅ ∨ ∅ ∈ 𝐴 ) )