Metamath Proof Explorer


Theorem ordnexbtwnsuc

Description: For any distinct pair of ordinals, if there is no ordinal between the lesser and the greater, the greater is the successor of the lesser. Lemma 1.16 of Schloeder p. 2. (Contributed by RP, 16-Jan-2025)

Ref Expression
Assertion ordnexbtwnsuc A B Ord B c On ¬ A c c B B = suc A

Proof

Step Hyp Ref Expression
1 ordelord Ord B A B Ord A
2 ordnbtwn Ord A ¬ A B B suc A
3 2 pm2.21d Ord A A B B suc A c On A c c B
4 3 expd Ord A A B B suc A c On A c c B
5 4 com12 A B Ord A B suc A c On A c c B
6 5 adantl Ord B A B Ord A B suc A c On A c c B
7 1 6 mpd Ord B A B B suc A c On A c c B
8 sucidg A B A suc A
9 8 adantl Ord B A B A suc A
10 ordelon Ord B A B A On
11 onsuc A On suc A On
12 10 11 syl Ord B A B suc A On
13 eleq2 c = suc A A c A suc A
14 eleq1 c = suc A c B suc A B
15 13 14 anbi12d c = suc A A c c B A suc A suc A B
16 15 adantl Ord B A B c = suc A A c c B A suc A suc A B
17 12 16 rspcedv Ord B A B A suc A suc A B c On A c c B
18 9 17 mpand Ord B A B suc A B c On A c c B
19 7 18 jaod Ord B A B B suc A suc A B c On A c c B
20 ralnex c On ¬ A c c B ¬ c On A c c B
21 20 biimpi c On ¬ A c c B ¬ c On A c c B
22 19 21 nsyli Ord B A B c On ¬ A c c B ¬ B suc A suc A B
23 ordsuci Ord A Ord suc A
24 1 23 syl Ord B A B Ord suc A
25 ordtri3 Ord B Ord suc A B = suc A ¬ B suc A suc A B
26 24 25 syldan Ord B A B B = suc A ¬ B suc A suc A B
27 22 26 sylibrd Ord B A B c On ¬ A c c B B = suc A
28 27 ancoms A B Ord B c On ¬ A c c B B = suc A