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

Metamath Proof Explorer

Theorem ordnbtwn

Description: There is no set between an ordinal class and its successor. Generalized Proposition 7.25 of TakeutiZaring p. 41. Lemma 1.15 of Schloeder p. 2. (Contributed by NM, 21-Jun-1998) (Proof shortened by JJ, 24-Sep-2021)

Ref Expression
Assertion ordnbtwn 
|- ( Ord A -> -. ( A e. B /\ B e. suc A ) )

Proof

Step Hyp Ref Expression
1 ordirr 
 |-  ( Ord A -> -. A e. A )
2 ordn2lp 
 |-  ( Ord A -> -. ( A e. B /\ B e. A ) )
3 pm2.24 
 |-  ( ( A e. B /\ B e. A ) -> ( -. ( A e. B /\ B e. A ) -> A e. A ) )
4 eleq2 
 |-  ( B = A -> ( A e. B <-> A e. A ) )
5 4 biimpac 
 |-  ( ( A e. B /\ B = A ) -> A e. A )
6 5 a1d 
 |-  ( ( A e. B /\ B = A ) -> ( -. ( A e. B /\ B e. A ) -> A e. A ) )
7 3 6 jaodan 
 |-  ( ( A e. B /\ ( B e. A \/ B = A ) ) -> ( -. ( A e. B /\ B e. A ) -> A e. A ) )
8 2 7 syl5com 
 |-  ( Ord A -> ( ( A e. B /\ ( B e. A \/ B = A ) ) -> A e. A ) )
9 1 8 mtod 
 |-  ( Ord A -> -. ( A e. B /\ ( B e. A \/ B = A ) ) )
10 elsuci 
 |-  ( B e. suc A -> ( B e. A \/ B = A ) )
11 10 anim2i 
 |-  ( ( A e. B /\ B e. suc A ) -> ( A e. B /\ ( B e. A \/ B = A ) ) )
12 9 11 nsyl 
 |-  ( Ord A -> -. ( A e. B /\ B e. suc A ) )