Metamath Proof Explorer

Theorem aleph1min

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

Ref Expression
Assertion aleph1min 
|- ( aleph ` 1o ) = |^| { x e. On | _om ~< x }

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 1 fveq2i 
 |-  ( aleph ` 1o ) = ( aleph ` suc (/) )
3 0elon 
 |-  (/) e. On
4 alephsuc 
 |-  ( (/) e. On -> ( aleph ` suc (/) ) = ( har ` ( aleph ` (/) ) ) )
5 3 4 ax-mp 
 |-  ( aleph ` suc (/) ) = ( har ` ( aleph ` (/) ) )
6 aleph0 
 |-  ( aleph ` (/) ) = _om
7 6 fveq2i 
 |-  ( har ` ( aleph ` (/) ) ) = ( har ` _om )
8 5 7 eqtri 
 |-  ( aleph ` suc (/) ) = ( har ` _om )
9 omelon 
 |-  _om e. On
10 onenon 
 |-  ( _om e. On -> _om e. dom card )
11 9 10 ax-mp 
 |-  _om e. dom card
12 harval2 
 |-  ( _om e. dom card -> ( har ` _om ) = |^| { x e. On | _om ~< x } )
13 11 12 ax-mp 
 |-  ( har ` _om ) = |^| { x e. On | _om ~< x }
14 8 13 eqtri 
 |-  ( aleph ` suc (/) ) = |^| { x e. On | _om ~< x }
15 2 14 eqtri 
 |-  ( aleph ` 1o ) = |^| { x e. On | _om ~< x }