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 𝐴 → ¬ ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ suc 𝐴 ) )

Proof

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