Metamath Proof Explorer

Theorem rankf

Description: The domain and range of the rank function. (Contributed by Mario Carneiro, 28-May-2013) (Revised by Mario Carneiro, 12-Sep-2013)

Ref Expression
Assertion rankf 
|- rank : U. ( R1 " On ) --> On

Proof

Step Hyp Ref Expression
1 df-rank 
 |-  rank = ( x e. _V |-> |^| { y e. On | x e. ( R1 ` suc y ) } )
2 1 funmpt2 
 |-  Fun rank
3 mptv 
 |-  ( x e. _V |-> |^| { y e. On | x e. ( R1 ` suc y ) } ) = { <. x , z >. | z = |^| { y e. On | x e. ( R1 ` suc y ) } }
4 1 3 eqtri 
 |-  rank = { <. x , z >. | z = |^| { y e. On | x e. ( R1 ` suc y ) } }
5 4 dmeqi 
 |-  dom rank = dom { <. x , z >. | z = |^| { y e. On | x e. ( R1 ` suc y ) } }
6 dmopab 
 |-  dom { <. x , z >. | z = |^| { y e. On | x e. ( R1 ` suc y ) } } = { x | E. z z = |^| { y e. On | x e. ( R1 ` suc y ) } }
7 abeq1 
 |-  ( { x | E. z z = |^| { y e. On | x e. ( R1 ` suc y ) } } = U. ( R1 " On ) <-> A. x ( E. z z = |^| { y e. On | x e. ( R1 ` suc y ) } <-> x e. U. ( R1 " On ) ) )
8 rankwflemb 
 |-  ( x e. U. ( R1 " On ) <-> E. y e. On x e. ( R1 ` suc y ) )
9 intexrab 
 |-  ( E. y e. On x e. ( R1 ` suc y ) <-> |^| { y e. On | x e. ( R1 ` suc y ) } e. _V )
10 isset 
 |-  ( |^| { y e. On | x e. ( R1 ` suc y ) } e. _V <-> E. z z = |^| { y e. On | x e. ( R1 ` suc y ) } )
11 8 9 10 3bitrri 
 |-  ( E. z z = |^| { y e. On | x e. ( R1 ` suc y ) } <-> x e. U. ( R1 " On ) )
12 7 11 mpgbir 
 |-  { x | E. z z = |^| { y e. On | x e. ( R1 ` suc y ) } } = U. ( R1 " On )
13 6 12 eqtri 
 |-  dom { <. x , z >. | z = |^| { y e. On | x e. ( R1 ` suc y ) } } = U. ( R1 " On )
14 5 13 eqtri 
 |-  dom rank = U. ( R1 " On )
15 df-fn 
 |-  ( rank Fn U. ( R1 " On ) <-> ( Fun rank /\ dom rank = U. ( R1 " On ) ) )
16 2 14 15 mpbir2an 
 |-  rank Fn U. ( R1 " On )
17 rabn0 
 |-  ( { y e. On | x e. ( R1 ` suc y ) } =/= (/) <-> E. y e. On x e. ( R1 ` suc y ) )
18 8 17 bitr4i 
 |-  ( x e. U. ( R1 " On ) <-> { y e. On | x e. ( R1 ` suc y ) } =/= (/) )
19 intex 
 |-  ( { y e. On | x e. ( R1 ` suc y ) } =/= (/) <-> |^| { y e. On | x e. ( R1 ` suc y ) } e. _V )
20 vex 
 |-  x e. _V
21 1 fvmpt2 
 |-  ( ( x e. _V /\ |^| { y e. On | x e. ( R1 ` suc y ) } e. _V ) -> ( rank ` x ) = |^| { y e. On | x e. ( R1 ` suc y ) } )
22 20 21 mpan 
 |-  ( |^| { y e. On | x e. ( R1 ` suc y ) } e. _V -> ( rank ` x ) = |^| { y e. On | x e. ( R1 ` suc y ) } )
23 19 22 sylbi 
 |-  ( { y e. On | x e. ( R1 ` suc y ) } =/= (/) -> ( rank ` x ) = |^| { y e. On | x e. ( R1 ` suc y ) } )
24 ssrab2 
 |-  { y e. On | x e. ( R1 ` suc y ) } C_ On
25 oninton 
 |-  ( ( { y e. On | x e. ( R1 ` suc y ) } C_ On /\ { y e. On | x e. ( R1 ` suc y ) } =/= (/) ) -> |^| { y e. On | x e. ( R1 ` suc y ) } e. On )
26 24 25 mpan 
 |-  ( { y e. On | x e. ( R1 ` suc y ) } =/= (/) -> |^| { y e. On | x e. ( R1 ` suc y ) } e. On )
27 23 26 eqeltrd 
 |-  ( { y e. On | x e. ( R1 ` suc y ) } =/= (/) -> ( rank ` x ) e. On )
28 18 27 sylbi 
 |-  ( x e. U. ( R1 " On ) -> ( rank ` x ) e. On )
29 28 rgen 
 |-  A. x e. U. ( R1 " On ) ( rank ` x ) e. On
30 ffnfv 
 |-  ( rank : U. ( R1 " On ) --> On <-> ( rank Fn U. ( R1 " On ) /\ A. x e. U. ( R1 " On ) ( rank ` x ) e. On ) )
31 16 29 30 mpbir2an 
 |-  rank : U. ( R1 " On ) --> On