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 ∈ B ∧ B ∈ suc ⁡ A

Proof

Step Hyp Ref Expression
1 ordirr ⊢ Ord ⁡ A → ¬ A ∈ A
2 ordn2lp ⊢ Ord ⁡ A → ¬ A ∈ B ∧ B ∈ A
3 pm2.24 ⊢ A ∈ B ∧ B ∈ A → ¬ A ∈ B ∧ B ∈ A → A ∈ A
4 eleq2 ⊢ B = A → A ∈ B ↔ A ∈ A
5 4 biimpac ⊢ A ∈ B ∧ B = A → A ∈ A
6 5 a1d ⊢ A ∈ B ∧ B = A → ¬ A ∈ B ∧ B ∈ A → A ∈ A
7 3 6 jaodan ⊢ A ∈ B ∧ B ∈ A ∨ B = A → ¬ A ∈ B ∧ B ∈ A → A ∈ A
8 2 7 syl5com ⊢ Ord ⁡ A → A ∈ B ∧ B ∈ A ∨ B = A → A ∈ A
9 1 8 mtod ⊢ Ord ⁡ A → ¬ A ∈ B ∧ B ∈ A ∨ B = A
10 elsuci ⊢ B ∈ suc ⁡ A → B ∈ A ∨ B = A
11 10 anim2i ⊢ A ∈ B ∧ B ∈ suc ⁡ A → A ∈ B ∧ B ∈ A ∨ B = A
12 9 11 nsyl ⊢ Ord ⁡ A → ¬ A ∈ B ∧ B ∈ suc ⁡ A