Theorem harsucnn

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

	Ref	Expression
Assertion	harsucnn	⊢ ( 𝐴 ∈ ω → ( har ‘ 𝐴 ) = suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
2		onenon	⊢ ( 𝐴 ∈ On → 𝐴 ∈ dom card )
3		harval2	⊢ ( 𝐴 ∈ dom card → ( har ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
4	1 2 3	3syl	⊢ ( 𝐴 ∈ ω → ( har ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } )
5		sucdom	⊢ ( 𝐴 ∈ ω → ( 𝐴 ≺ 𝑥 ↔ suc 𝐴 ≼ 𝑥 ) )
6	5	adantr	⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( 𝐴 ≺ 𝑥 ↔ suc 𝐴 ≼ 𝑥 ) )
7		peano2	⊢ ( 𝐴 ∈ ω → suc 𝐴 ∈ ω )
8		nndomog	⊢ ( ( suc 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( suc 𝐴 ≼ 𝑥 ↔ suc 𝐴 ⊆ 𝑥 ) )
9	7 8	sylan	⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( suc 𝐴 ≼ 𝑥 ↔ suc 𝐴 ⊆ 𝑥 ) )
10	6 9	bitrd	⊢ ( ( 𝐴 ∈ ω ∧ 𝑥 ∈ On ) → ( 𝐴 ≺ 𝑥 ↔ suc 𝐴 ⊆ 𝑥 ) )
11	10	rabbidva	⊢ ( 𝐴 ∈ ω → { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } )
12	11	inteqd	⊢ ( 𝐴 ∈ ω → ∩ { 𝑥 ∈ On ∣ 𝐴 ≺ 𝑥 } = ∩ { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } )
13		nnon	⊢ ( suc 𝐴 ∈ ω → suc 𝐴 ∈ On )
14		intmin	⊢ ( suc 𝐴 ∈ On → ∩ { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } = suc 𝐴 )
15	7 13 14	3syl	⊢ ( 𝐴 ∈ ω → ∩ { 𝑥 ∈ On ∣ suc 𝐴 ⊆ 𝑥 } = suc 𝐴 )
16	4 12 15	3eqtrd	⊢ ( 𝐴 ∈ ω → ( har ‘ 𝐴 ) = suc 𝐴 )