Metamath Proof Explorer

Theorem orddif0suc

Description: For any distinct pair of ordinals, if the set difference between the greater and the successor of the lesser is empty, the greater is the successor of the lesser. Lemma 1.16 of Schloeder p. 2. (Contributed by RP, 17-Jan-2025)

Ref Expression
Assertion orddif0suc ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( ( 𝐵 ∖ suc 𝐴 ) = ∅ → 𝐵 = suc 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → Ord 𝐵 )
2 ordelon ⊢ ( ( Ord 𝐵 ∧ 𝐴 ∈ 𝐵 ) → 𝐴 ∈ On )
3 2 ancoms ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → 𝐴 ∈ On )
4 ordeldifsucon ⊢ ( ( Ord 𝐵 ∧ 𝐴 ∈ On ) → ( 𝑐 ∈ ( 𝐵 ∖ suc 𝐴 ) ↔ ( 𝑐 ∈ 𝐵 ∧ 𝐴 ∈ 𝑐 ) ) )
5 1 3 4 syl2anc ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( 𝑐 ∈ ( 𝐵 ∖ suc 𝐴 ) ↔ ( 𝑐 ∈ 𝐵 ∧ 𝐴 ∈ 𝑐 ) ) )
6 5 biancomd ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( 𝑐 ∈ ( 𝐵 ∖ suc 𝐴 ) ↔ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ) )
7 ordelon ⊢ ( ( Ord 𝐵 ∧ 𝑐 ∈ 𝐵 ) → 𝑐 ∈ On )
8 7 ad2ant2l ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) ∧ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ) → 𝑐 ∈ On )
9 8 ex ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) → 𝑐 ∈ On ) )
10 9 pm4.71rd ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ↔ ( 𝑐 ∈ On ∧ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ) ) )
11 df-an ⊢ ( ( 𝑐 ∈ On ∧ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ) ↔ ¬ ( 𝑐 ∈ On → ¬ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ) )
12 10 11 bitrdi ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ↔ ¬ ( 𝑐 ∈ On → ¬ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ) ) )
13 6 12 bitr2d ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( ¬ ( 𝑐 ∈ On → ¬ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ) ↔ 𝑐 ∈ ( 𝐵 ∖ suc 𝐴 ) ) )
14 13 con1bid ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( ¬ 𝑐 ∈ ( 𝐵 ∖ suc 𝐴 ) ↔ ( 𝑐 ∈ On → ¬ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ) ) )
15 14 albidv ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( ∀ 𝑐 ¬ 𝑐 ∈ ( 𝐵 ∖ suc 𝐴 ) ↔ ∀ 𝑐 ( 𝑐 ∈ On → ¬ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ) ) )
16 eq0 ⊢ ( ( 𝐵 ∖ suc 𝐴 ) = ∅ ↔ ∀ 𝑐 ¬ 𝑐 ∈ ( 𝐵 ∖ suc 𝐴 ) )
17 df-ral ⊢ ( ∀ 𝑐 ∈ On ¬ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ↔ ∀ 𝑐 ( 𝑐 ∈ On → ¬ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ) )
18 15 16 17 3bitr4g ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( ( 𝐵 ∖ suc 𝐴 ) = ∅ ↔ ∀ 𝑐 ∈ On ¬ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) ) )
19 ordnexbtwnsuc ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( ∀ 𝑐 ∈ On ¬ ( 𝐴 ∈ 𝑐 ∧ 𝑐 ∈ 𝐵 ) → 𝐵 = suc 𝐴 ) )
20 18 19 sylbid ⊢ ( ( 𝐴 ∈ 𝐵 ∧ Ord 𝐵 ) → ( ( 𝐵 ∖ suc 𝐴 ) = ∅ → 𝐵 = suc 𝐴 ) )