Metamath Proof Explorer


Theorem alephfplem1

Description: Lemma for alephfp . (Contributed by NM, 6-Nov-2004)

Ref Expression
Hypothesis alephfplem.1
|- H = ( rec ( aleph , _om ) |` _om )
Assertion alephfplem1
|- ( H ` (/) ) e. ran aleph

Proof

Step Hyp Ref Expression
1 alephfplem.1
 |-  H = ( rec ( aleph , _om ) |` _om )
2 omex
 |-  _om e. _V
3 fr0g
 |-  ( _om e. _V -> ( ( rec ( aleph , _om ) |` _om ) ` (/) ) = _om )
4 2 3 ax-mp
 |-  ( ( rec ( aleph , _om ) |` _om ) ` (/) ) = _om
5 1 fveq1i
 |-  ( H ` (/) ) = ( ( rec ( aleph , _om ) |` _om ) ` (/) )
6 aleph0
 |-  ( aleph ` (/) ) = _om
7 4 5 6 3eqtr4i
 |-  ( H ` (/) ) = ( aleph ` (/) )
8 alephfnon
 |-  aleph Fn On
9 0elon
 |-  (/) e. On
10 fnfvelrn
 |-  ( ( aleph Fn On /\ (/) e. On ) -> ( aleph ` (/) ) e. ran aleph )
11 8 9 10 mp2an
 |-  ( aleph ` (/) ) e. ran aleph
12 7 11 eqeltri
 |-  ( H ` (/) ) e. ran aleph