Theorem onnbtwn

Description: There is no set between an ordinal number and its successor. Proposition 7.25 of TakeutiZaring p. 41. (Contributed by NM, 9-Jun-1994)

	Ref	Expression
Assertion	onnbtwn	$$⊢A\in \mathrm{On}\to \neg \left(A\in B\wedge B\in \mathrm{suc}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
2		ordnbtwn	$$⊢\mathrm{Ord}A\to \neg \left(A\in B\wedge B\in \mathrm{suc}A\right)$$
3	1 2	syl	$$⊢A\in \mathrm{On}\to \neg \left(A\in B\wedge B\in \mathrm{suc}A\right)$$