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∈OnA∈c∧c∈B
4 3 expd ⊢Ord⁡A→A∈B→B∈suc⁡A→∃c∈OnA∈c∧c∈B
5 4 com12 ⊢A∈B→Ord⁡A→B∈suc⁡A→∃c∈OnA∈c∧c∈B
6 5 adantl ⊢Ord⁡B∧A∈B→Ord⁡A→B∈suc⁡A→∃c∈OnA∈c∧c∈B
7 1 6 mpd ⊢Ord⁡B∧A∈B→B∈suc⁡A→∃c∈OnA∈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∈OnA∈c∧c∈B
18 9 17 mpand ⊢Ord⁡B∧A∈B→suc⁡A∈B→∃c∈OnA∈c∧c∈B
19 7 18 jaod ⊢Ord⁡B∧A∈B→B∈suc⁡A∨suc⁡A∈B→∃c∈OnA∈c∧c∈B
20 ralnex ⊢∀c∈On¬A∈c∧c∈B↔¬∃c∈OnA∈c∧c∈B
21 20 biimpi ⊢∀c∈On¬A∈c∧c∈B→¬∃c∈OnA∈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