Theorem aleph1min

Description: ( aleph1o ) is the least uncountable ordinal. (Contributed by RP, 18-Nov-2023)

	Ref	Expression
Assertion	aleph1min	⊢ ( ℵ ‘ 1o ) = ∩ { 𝑥 ∈ On ∣ ω ≺ 𝑥 }

Proof

Step	Hyp	Ref	Expression
1		df-1o	⊢ 1o = suc ∅
2	1	fveq2i	⊢ ( ℵ ‘ 1o ) = ( ℵ ‘ suc ∅ )
3		0elon	⊢ ∅ ∈ On
4		alephsuc	⊢ ( ∅ ∈ On → ( ℵ ‘ suc ∅ ) = ( har ‘ ( ℵ ‘ ∅ ) ) )
5	3 4	ax-mp	⊢ ( ℵ ‘ suc ∅ ) = ( har ‘ ( ℵ ‘ ∅ ) )
6		aleph0	⊢ ( ℵ ‘ ∅ ) = ω
7	6	fveq2i	⊢ ( har ‘ ( ℵ ‘ ∅ ) ) = ( har ‘ ω )
8	5 7	eqtri	⊢ ( ℵ ‘ suc ∅ ) = ( har ‘ ω )
9		omelon	⊢ ω ∈ On
10		onenon	⊢ ( ω ∈ On → ω ∈ dom card )
11	9 10	ax-mp	⊢ ω ∈ dom card
12		harval2	⊢ ( ω ∈ dom card → ( har ‘ ω ) = ∩ { 𝑥 ∈ On ∣ ω ≺ 𝑥 } )
13	11 12	ax-mp	⊢ ( har ‘ ω ) = ∩ { 𝑥 ∈ On ∣ ω ≺ 𝑥 }
14	8 13	eqtri	⊢ ( ℵ ‘ suc ∅ ) = ∩ { 𝑥 ∈ On ∣ ω ≺ 𝑥 }
15	2 14	eqtri	⊢ ( ℵ ‘ 1o ) = ∩ { 𝑥 ∈ On ∣ ω ≺ 𝑥 }