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

Metamath Proof Explorer

Theorem ordsssuc2

Description: An ordinal subset of an ordinal number belongs to its successor. (Contributed by NM, 1-Feb-2005) (Proof shortened by Andrew Salmon, 12-Aug-2011)

Ref Expression
Assertion ordsssuc2 
|- ( ( Ord A /\ B e. On ) -> ( A C_ B <-> A e. suc B ) )

Proof

Step Hyp Ref Expression
1 elong 
 |-  ( A e. _V -> ( A e. On <-> Ord A ) )
2 1 biimprd 
 |-  ( A e. _V -> ( Ord A -> A e. On ) )
3 2 anim1d 
 |-  ( A e. _V -> ( ( Ord A /\ B e. On ) -> ( A e. On /\ B e. On ) ) )
4 onsssuc 
 |-  ( ( A e. On /\ B e. On ) -> ( A C_ B <-> A e. suc B ) )
5 3 4 syl6 
 |-  ( A e. _V -> ( ( Ord A /\ B e. On ) -> ( A C_ B <-> A e. suc B ) ) )
6 annim 
 |-  ( ( B e. On /\ -. A e. _V ) <-> -. ( B e. On -> A e. _V ) )
7 ssexg 
 |-  ( ( A C_ B /\ B e. On ) -> A e. _V )
8 7 ex 
 |-  ( A C_ B -> ( B e. On -> A e. _V ) )
9 elex 
 |-  ( A e. suc B -> A e. _V )
10 9 a1d 
 |-  ( A e. suc B -> ( B e. On -> A e. _V ) )
11 8 10 pm5.21ni 
 |-  ( -. ( B e. On -> A e. _V ) -> ( A C_ B <-> A e. suc B ) )
12 6 11 sylbi 
 |-  ( ( B e. On /\ -. A e. _V ) -> ( A C_ B <-> A e. suc B ) )
13 12 expcom 
 |-  ( -. A e. _V -> ( B e. On -> ( A C_ B <-> A e. suc B ) ) )
14 13 adantld 
 |-  ( -. A e. _V -> ( ( Ord A /\ B e. On ) -> ( A C_ B <-> A e. suc B ) ) )
15 5 14 pm2.61i 
 |-  ( ( Ord A /\ B e. On ) -> ( A C_ B <-> A e. suc B ) )