This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )