Metamath Proof Explorer

Theorem ordsucss

Description: The successor of an element of an ordinal class is a subset of it. (Contributed by NM, 21-Jun-1998)

Ref Expression
Assertion ordsucss 
|- ( Ord B -> ( A e. B -> suc A C_ B ) )

Proof

Step Hyp Ref Expression
1 ordelord 
 |-  ( ( Ord B /\ A e. B ) -> Ord A )
2 ordnbtwn 
 |-  ( Ord A -> -. ( A e. B /\ B e. suc A ) )
3 imnan 
 |-  ( ( A e. B -> -. B e. suc A ) <-> -. ( A e. B /\ B e. suc A ) )
4 2 3 sylibr 
 |-  ( Ord A -> ( A e. B -> -. B e. suc A ) )
5 4 adantr 
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B -> -. B e. suc A ) )
6 ordsuc 
 |-  ( Ord A <-> Ord suc A )
7 ordtri1 
 |-  ( ( Ord suc A /\ Ord B ) -> ( suc A C_ B <-> -. B e. suc A ) )
8 6 7 sylanb 
 |-  ( ( Ord A /\ Ord B ) -> ( suc A C_ B <-> -. B e. suc A ) )
9 5 8 sylibrd 
 |-  ( ( Ord A /\ Ord B ) -> ( A e. B -> suc A C_ B ) )
10 1 9 sylan 
 |-  ( ( ( Ord B /\ A e. B ) /\ Ord B ) -> ( A e. B -> suc A C_ B ) )
11 10 exp31 
 |-  ( Ord B -> ( A e. B -> ( Ord B -> ( A e. B -> suc A C_ B ) ) ) )
12 11 pm2.43b 
 |-  ( A e. B -> ( Ord B -> ( A e. B -> suc A C_ B ) ) )
13 12 pm2.43b 
 |-  ( Ord B -> ( A e. B -> suc A C_ B ) )