Metamath Proof Explorer

Theorem onsucf1olem

Description: The successor operation is bijective between the ordinals and the class of successor ordinals. Lemma 1.17 of Schloeder p. 2. (Contributed by RP, 18-Jan-2025)

Ref Expression
Assertion onsucf1olem ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → ∃! 𝑏 ∈ On 𝐴 = suc 𝑏 )

Proof

Step Hyp Ref Expression
1 onuni ⊢ ( 𝐴 ∈ On → ∪ 𝐴 ∈ On )
2 1 3ad2ant1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → ∪ 𝐴 ∈ On )
3 eloni ⊢ ( 𝐴 ∈ On → Ord 𝐴 )
4 unizlim ⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ↔ ( 𝐴 = ∅ ∨ Lim 𝐴 ) ) )
5 oran ⊢ ( ( 𝐴 = ∅ ∨ Lim 𝐴 ) ↔ ¬ ( ¬ 𝐴 = ∅ ∧ ¬ Lim 𝐴 ) )
6 df-ne ⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
7 6 anbi1i ⊢ ( ( 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) ↔ ( ¬ 𝐴 = ∅ ∧ ¬ Lim 𝐴 ) )
8 5 7 xchbinxr ⊢ ( ( 𝐴 = ∅ ∨ Lim 𝐴 ) ↔ ¬ ( 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) )
9 4 8 bitrdi ⊢ ( Ord 𝐴 → ( 𝐴 = ∪ 𝐴 ↔ ¬ ( 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) ) )
10 3 9 syl ⊢ ( 𝐴 ∈ On → ( 𝐴 = ∪ 𝐴 ↔ ¬ ( 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) ) )
11 pm2.21 ⊢ ( ¬ ( 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → ( ( 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → 𝐴 = suc ∪ 𝐴 ) )
12 10 11 biimtrdi ⊢ ( 𝐴 ∈ On → ( 𝐴 = ∪ 𝐴 → ( ( 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → 𝐴 = suc ∪ 𝐴 ) ) )
13 12 com23 ⊢ ( 𝐴 ∈ On → ( ( 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → ( 𝐴 = ∪ 𝐴 → 𝐴 = suc ∪ 𝐴 ) ) )
14 13 3impib ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → ( 𝐴 = ∪ 𝐴 → 𝐴 = suc ∪ 𝐴 ) )
15 idd ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → ( 𝐴 = suc ∪ 𝐴 → 𝐴 = suc ∪ 𝐴 ) )
16 onuniorsuc ⊢ ( 𝐴 ∈ On → ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 ) )
17 16 3ad2ant1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → ( 𝐴 = ∪ 𝐴 ∨ 𝐴 = suc ∪ 𝐴 ) )
18 14 15 17 mpjaod ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → 𝐴 = suc ∪ 𝐴 )
19 2 18 jca ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → ( ∪ 𝐴 ∈ On ∧ 𝐴 = suc ∪ 𝐴 ) )
20 eleq1 ⊢ ( 𝑏 = ∪ 𝐴 → ( 𝑏 ∈ On ↔ ∪ 𝐴 ∈ On ) )
21 suceq ⊢ ( 𝑏 = ∪ 𝐴 → suc 𝑏 = suc ∪ 𝐴 )
22 21 eqeq2d ⊢ ( 𝑏 = ∪ 𝐴 → ( 𝐴 = suc 𝑏 ↔ 𝐴 = suc ∪ 𝐴 ) )
23 20 22 anbi12d ⊢ ( 𝑏 = ∪ 𝐴 → ( ( 𝑏 ∈ On ∧ 𝐴 = suc 𝑏 ) ↔ ( ∪ 𝐴 ∈ On ∧ 𝐴 = suc ∪ 𝐴 ) ) )
24 2 19 23 spcedv ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → ∃ 𝑏 ( 𝑏 ∈ On ∧ 𝐴 = suc 𝑏 ) )
25 onsucf1lem ⊢ ( 𝐴 ∈ On → ∃* 𝑏 ∈ On 𝐴 = suc 𝑏 )
26 25 3ad2ant1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → ∃* 𝑏 ∈ On 𝐴 = suc 𝑏 )
27 df-eu ⊢ ( ∃! 𝑏 ( 𝑏 ∈ On ∧ 𝐴 = suc 𝑏 ) ↔ ( ∃ 𝑏 ( 𝑏 ∈ On ∧ 𝐴 = suc 𝑏 ) ∧ ∃* 𝑏 ( 𝑏 ∈ On ∧ 𝐴 = suc 𝑏 ) ) )
28 df-reu ⊢ ( ∃! 𝑏 ∈ On 𝐴 = suc 𝑏 ↔ ∃! 𝑏 ( 𝑏 ∈ On ∧ 𝐴 = suc 𝑏 ) )
29 df-rmo ⊢ ( ∃* 𝑏 ∈ On 𝐴 = suc 𝑏 ↔ ∃* 𝑏 ( 𝑏 ∈ On ∧ 𝐴 = suc 𝑏 ) )
30 29 anbi2i ⊢ ( ( ∃ 𝑏 ( 𝑏 ∈ On ∧ 𝐴 = suc 𝑏 ) ∧ ∃* 𝑏 ∈ On 𝐴 = suc 𝑏 ) ↔ ( ∃ 𝑏 ( 𝑏 ∈ On ∧ 𝐴 = suc 𝑏 ) ∧ ∃* 𝑏 ( 𝑏 ∈ On ∧ 𝐴 = suc 𝑏 ) ) )
31 27 28 30 3bitr4i ⊢ ( ∃! 𝑏 ∈ On 𝐴 = suc 𝑏 ↔ ( ∃ 𝑏 ( 𝑏 ∈ On ∧ 𝐴 = suc 𝑏 ) ∧ ∃* 𝑏 ∈ On 𝐴 = suc 𝑏 ) )
32 24 26 31 sylanbrc ⊢ ( ( 𝐴 ∈ On ∧ 𝐴 ≠ ∅ ∧ ¬ Lim 𝐴 ) → ∃! 𝑏 ∈ On 𝐴 = suc 𝑏 )