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