This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐴 ∈ ω → ( 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 𝐴 )