Theorem ordnbtwn

Description: There is no set between an ordinal class and its successor. Generalized Proposition 7.25 of TakeutiZaring p. 41. (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 ) )