Metamath Proof Explorer

Theorem harsucnn

Description: The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023)

Ref Expression
Assertion harsucnn ⊢ A ∈ ω → har ⁡ A = suc ⁡ A

Proof

Step Hyp Ref Expression
1 nnon ⊢ A ∈ ω → A ∈ On
2 onenon ⊢ A ∈ On → A ∈ dom ⁡ card
3 harval2 ⊢ A ∈ dom ⁡ card → har ⁡ A = ⋂ x ∈ On | A ≺ x
4 1 2 3 3syl ⊢ A ∈ ω → har ⁡ A = ⋂ x ∈ On | A ≺ x
5 sucdom ⊢ A ∈ ω → A ≺ x ↔ suc ⁡ A ≼ x
6 5 adantr ⊢ A ∈ ω ∧ x ∈ On → A ≺ x ↔ suc ⁡ A ≼ x
7 peano2 ⊢ A ∈ ω → suc ⁡ A ∈ ω
8 nndomog ⊢ suc ⁡ A ∈ ω ∧ x ∈ On → suc ⁡ A ≼ x ↔ suc ⁡ A ⊆ x
9 7 8 sylan ⊢ A ∈ ω ∧ x ∈ On → suc ⁡ A ≼ x ↔ suc ⁡ A ⊆ x
10 6 9 bitrd ⊢ A ∈ ω ∧ x ∈ On → A ≺ x ↔ suc ⁡ A ⊆ x
11 10 rabbidva ⊢ A ∈ ω → x ∈ On | A ≺ x = x ∈ On | suc ⁡ A ⊆ x
12 11 inteqd ⊢ A ∈ ω → ⋂ x ∈ On | A ≺ x = ⋂ x ∈ On | suc ⁡ A ⊆ x
13 nnon ⊢ suc ⁡ A ∈ ω → suc ⁡ A ∈ On
14 intmin ⊢ suc ⁡ A ∈ On → ⋂ x ∈ On | suc ⁡ A ⊆ x = suc ⁡ A
15 7 13 14 3syl ⊢ A ∈ ω → ⋂ x ∈ On | suc ⁡ A ⊆ x = suc ⁡ A
16 4 12 15 3eqtrd ⊢ A ∈ ω → har ⁡ A = suc ⁡ A