Metamath Proof Explorer

Theorem onsucf1lem

Description: For ordinals, the successor operation is injective, so there is at most one ordinal that a given ordinal could be the successor of. Lemma 1.17 of Schloeder p. 2. (Contributed by RP, 18-Jan-2025)

Ref Expression
Assertion onsucf1lem ⊢ A ∈ On → ∃* b ∈ On A = suc ⁡ b

Proof

Step Hyp Ref Expression
1 onuni ⊢ A ∈ On → ⋃ A ∈ On
2 onsucuni2 ⊢ A ∈ On ∧ A = suc ⁡ b → suc ⁡ ⋃ A = A
3 2 adantlr ⊢ A ∈ On ∧ b ∈ On ∧ A = suc ⁡ b → suc ⁡ ⋃ A = A
4 simpr ⊢ A ∈ On ∧ b ∈ On ∧ A = suc ⁡ b → A = suc ⁡ b
5 3 4 eqtr2d ⊢ A ∈ On ∧ b ∈ On ∧ A = suc ⁡ b → suc ⁡ b = suc ⁡ ⋃ A
6 1 anim1i ⊢ A ∈ On ∧ b ∈ On → ⋃ A ∈ On ∧ b ∈ On
7 6 adantr ⊢ A ∈ On ∧ b ∈ On ∧ A = suc ⁡ b → ⋃ A ∈ On ∧ b ∈ On
8 7 ancomd ⊢ A ∈ On ∧ b ∈ On ∧ A = suc ⁡ b → b ∈ On ∧ ⋃ A ∈ On
9 suc11 ⊢ b ∈ On ∧ ⋃ A ∈ On → suc ⁡ b = suc ⁡ ⋃ A ↔ b = ⋃ A
10 8 9 syl ⊢ A ∈ On ∧ b ∈ On ∧ A = suc ⁡ b → suc ⁡ b = suc ⁡ ⋃ A ↔ b = ⋃ A
11 5 10 mpbid ⊢ A ∈ On ∧ b ∈ On ∧ A = suc ⁡ b → b = ⋃ A
12 11 ex ⊢ A ∈ On ∧ b ∈ On → A = suc ⁡ b → b = ⋃ A
13 12 ralrimiva ⊢ A ∈ On → ∀ b ∈ On A = suc ⁡ b → b = ⋃ A
14 eqeq2 ⊢ c = ⋃ A → b = c ↔ b = ⋃ A
15 14 imbi2d ⊢ c = ⋃ A → A = suc ⁡ b → b = c ↔ A = suc ⁡ b → b = ⋃ A
16 15 ralbidv ⊢ c = ⋃ A → ∀ b ∈ On A = suc ⁡ b → b = c ↔ ∀ b ∈ On A = suc ⁡ b → b = ⋃ A
17 1 13 16 spcedv ⊢ A ∈ On → ∃ c ∀ b ∈ On A = suc ⁡ b → b = c
18 nfv ⊢ Ⅎ c A = suc ⁡ b
19 18 rmo2 ⊢ ∃* b ∈ On A = suc ⁡ b ↔ ∃ c ∀ b ∈ On A = suc ⁡ b → b = c
20 17 19 sylibr ⊢ A ∈ On → ∃* b ∈ On A = suc ⁡ b