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

Metamath Proof Explorer

Theorem orddif

Description: Ordinal derived from its successor. (Contributed by NM, 20-May-1998)

Ref Expression
Assertion orddif 
|- ( Ord A -> A = ( suc A \ { A } ) )

Proof

Step Hyp Ref Expression
1 orddisj 
 |-  ( Ord A -> ( A i^i { A } ) = (/) )
2 disj3 
 |-  ( ( A i^i { A } ) = (/) <-> A = ( A \ { A } ) )
3 df-suc 
 |-  suc A = ( A u. { A } )
4 3 difeq1i 
 |-  ( suc A \ { A } ) = ( ( A u. { A } ) \ { A } )
5 difun2 
 |-  ( ( A u. { A } ) \ { A } ) = ( A \ { A } )
6 4 5 eqtri 
 |-  ( suc A \ { A } ) = ( A \ { A } )
7 6 eqeq2i 
 |-  ( A = ( suc A \ { A } ) <-> A = ( A \ { A } ) )
8 2 7 bitr4i 
 |-  ( ( A i^i { A } ) = (/) <-> A = ( suc A \ { A } ) )
9 1 8 sylib 
 |-  ( Ord A -> A = ( suc A \ { A } ) )