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