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

Metamath Proof Explorer

Theorem ordsucsssuc

Description: The subclass relationship between two ordinal classes is inherited by their successors. (Contributed by NM, 4-Oct-2003)

Ref Expression
Assertion ordsucsssuc 
|- ( ( Ord A /\ Ord B ) -> ( A C_ B <-> suc A C_ suc B ) )

Proof

Step Hyp Ref Expression
1 ordsucelsuc 
 |-  ( Ord A -> ( B e. A <-> suc B e. suc A ) )
2 1 notbid 
 |-  ( Ord A -> ( -. B e. A <-> -. suc B e. suc A ) )
3 2 adantr 
 |-  ( ( Ord A /\ Ord B ) -> ( -. B e. A <-> -. suc B e. suc A ) )
4 ordtri1 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B e. A ) )
5 ordsuc 
 |-  ( Ord A <-> Ord suc A )
6 ordsuc 
 |-  ( Ord B <-> Ord suc B )
7 ordtri1 
 |-  ( ( Ord suc A /\ Ord suc B ) -> ( suc A C_ suc B <-> -. suc B e. suc A ) )
8 5 6 7 syl2anb 
 |-  ( ( Ord A /\ Ord B ) -> ( suc A C_ suc B <-> -. suc B e. suc A ) )
9 3 4 8 3bitr4d 
 |-  ( ( Ord A /\ Ord B ) -> ( A C_ B <-> suc A C_ suc B ) )