Metamath Proof Explorer

Theorem bdayimaon

Description: Lemma for full-eta properties. The successor of the union of the image of the birthday function under a set is an ordinal. (Contributed by Scott Fenton, 20-Aug-2011)

Ref Expression
Assertion bdayimaon 
|- ( A e. V -> suc U. ( bday " A ) e. On )

Proof

Step Hyp Ref Expression
1 bdayfo 
 |-  bday : No -onto-> On
2 fofun 
 |-  ( bday : No -onto-> On -> Fun bday )
3 1 2 ax-mp 
 |-  Fun bday
4 funimaexg 
 |-  ( ( Fun bday /\ A e. V ) -> ( bday " A ) e. _V )
5 3 4 mpan 
 |-  ( A e. V -> ( bday " A ) e. _V )
6 5 uniexd 
 |-  ( A e. V -> U. ( bday " A ) e. _V )
7 imassrn 
 |-  ( bday " A ) C_ ran bday
8 forn 
 |-  ( bday : No -onto-> On -> ran bday = On )
9 1 8 ax-mp 
 |-  ran bday = On
10 7 9 sseqtri 
 |-  ( bday " A ) C_ On
11 ssorduni 
 |-  ( ( bday " A ) C_ On -> Ord U. ( bday " A ) )
12 10 11 ax-mp 
 |-  Ord U. ( bday " A )
13 6 12 jctil 
 |-  ( A e. V -> ( Ord U. ( bday " A ) /\ U. ( bday " A ) e. _V ) )
14 elon2 
 |-  ( U. ( bday " A ) e. On <-> ( Ord U. ( bday " A ) /\ U. ( bday " A ) e. _V ) )
15 sucelon 
 |-  ( U. ( bday " A ) e. On <-> suc U. ( bday " A ) e. On )
16 14 15 bitr3i 
 |-  ( ( Ord U. ( bday " A ) /\ U. ( bday " A ) e. _V ) <-> suc U. ( bday " A ) e. On )
17 13 16 sylib 
 |-  ( A e. V -> suc U. ( bday " A ) e. On )