Metamath Proof Explorer

Theorem alephfplem4

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

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

Proof

Step Hyp Ref Expression
1 alephfplem.1 
 |-  H = ( rec ( aleph , _om ) |` _om )
2 frfnom 
 |-  ( rec ( aleph , _om ) |` _om ) Fn _om
3 1 fneq1i 
 |-  ( H Fn _om <-> ( rec ( aleph , _om ) |` _om ) Fn _om )
4 2 3 mpbir 
 |-  H Fn _om
5 1 alephfplem3 
 |-  ( z e. _om -> ( H ` z ) e. ran aleph )
6 5 rgen 
 |-  A. z e. _om ( H ` z ) e. ran aleph
7 ffnfv 
 |-  ( H : _om --> ran aleph <-> ( H Fn _om /\ A. z e. _om ( H ` z ) e. ran aleph ) )
8 4 6 7 mpbir2an 
 |-  H : _om --> ran aleph
9 ssun2 
 |-  ran aleph C_ ( _om u. ran aleph )
10 fss 
 |-  ( ( H : _om --> ran aleph /\ ran aleph C_ ( _om u. ran aleph ) ) -> H : _om --> ( _om u. ran aleph ) )
11 8 9 10 mp2an 
 |-  H : _om --> ( _om u. ran aleph )
12 peano1 
 |-  (/) e. _om
13 1 alephfplem1 
 |-  ( H ` (/) ) e. ran aleph
14 fveq2 
 |-  ( z = (/) -> ( H ` z ) = ( H ` (/) ) )
15 14 eleq1d 
 |-  ( z = (/) -> ( ( H ` z ) e. ran aleph <-> ( H ` (/) ) e. ran aleph ) )
16 15 rspcev 
 |-  ( ( (/) e. _om /\ ( H ` (/) ) e. ran aleph ) -> E. z e. _om ( H ` z ) e. ran aleph )
17 12 13 16 mp2an 
 |-  E. z e. _om ( H ` z ) e. ran aleph
18 omex 
 |-  _om e. _V
19 cardinfima 
 |-  ( _om e. _V -> ( ( H : _om --> ( _om u. ran aleph ) /\ E. z e. _om ( H ` z ) e. ran aleph ) -> U. ( H " _om ) e. ran aleph ) )
20 18 19 ax-mp 
 |-  ( ( H : _om --> ( _om u. ran aleph ) /\ E. z e. _om ( H ` z ) e. ran aleph ) -> U. ( H " _om ) e. ran aleph )
21 11 17 20 mp2an 
 |-  U. ( H " _om ) e. ran aleph