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