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

Metamath Proof Explorer

Theorem orduniorsuc

Description: An ordinal class is either its union or the successor of its union. If we adopt the view that zero is a limit ordinal, this means every ordinal class is either a limit or a successor. (Contributed by NM, 13-Sep-2003)

Ref Expression
Assertion orduniorsuc 
|- ( Ord A -> ( A = U. A \/ A = suc U. A ) )

Proof

Step Hyp Ref Expression
1 orduniss 
 |-  ( Ord A -> U. A C_ A )
2 orduni 
 |-  ( Ord A -> Ord U. A )
3 ordelssne 
 |-  ( ( Ord U. A /\ Ord A ) -> ( U. A e. A <-> ( U. A C_ A /\ U. A =/= A ) ) )
4 2 3 mpancom 
 |-  ( Ord A -> ( U. A e. A <-> ( U. A C_ A /\ U. A =/= A ) ) )
5 4 biimprd 
 |-  ( Ord A -> ( ( U. A C_ A /\ U. A =/= A ) -> U. A e. A ) )
6 1 5 mpand 
 |-  ( Ord A -> ( U. A =/= A -> U. A e. A ) )
7 ordsucss 
 |-  ( Ord A -> ( U. A e. A -> suc U. A C_ A ) )
8 6 7 syld 
 |-  ( Ord A -> ( U. A =/= A -> suc U. A C_ A ) )
9 ordsucuni 
 |-  ( Ord A -> A C_ suc U. A )
10 8 9 jctild 
 |-  ( Ord A -> ( U. A =/= A -> ( A C_ suc U. A /\ suc U. A C_ A ) ) )
11 df-ne 
 |-  ( A =/= U. A <-> -. A = U. A )
12 necom 
 |-  ( A =/= U. A <-> U. A =/= A )
13 11 12 bitr3i 
 |-  ( -. A = U. A <-> U. A =/= A )
14 eqss 
 |-  ( A = suc U. A <-> ( A C_ suc U. A /\ suc U. A C_ A ) )
15 10 13 14 3imtr4g 
 |-  ( Ord A -> ( -. A = U. A -> A = suc U. A ) )
16 15 orrd 
 |-  ( Ord A -> ( A = U. A \/ A = suc U. A ) )