Metamath Proof Explorer


Theorem r1funlim

Description: The cumulative hierarchy of sets function is a function on a limit ordinal. (This weak form of r1fnon avoids ax-rep .) (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion r1funlim
|- ( Fun R1 /\ Lim dom R1 )

Proof

Step Hyp Ref Expression
1 rdgfun
 |-  Fun rec ( ( x e. _V |-> ~P x ) , (/) )
2 df-r1
 |-  R1 = rec ( ( x e. _V |-> ~P x ) , (/) )
3 2 funeqi
 |-  ( Fun R1 <-> Fun rec ( ( x e. _V |-> ~P x ) , (/) ) )
4 1 3 mpbir
 |-  Fun R1
5 rdgdmlim
 |-  Lim dom rec ( ( x e. _V |-> ~P x ) , (/) )
6 2 dmeqi
 |-  dom R1 = dom rec ( ( x e. _V |-> ~P x ) , (/) )
7 limeq
 |-  ( dom R1 = dom rec ( ( x e. _V |-> ~P x ) , (/) ) -> ( Lim dom R1 <-> Lim dom rec ( ( x e. _V |-> ~P x ) , (/) ) ) )
8 6 7 ax-mp
 |-  ( Lim dom R1 <-> Lim dom rec ( ( x e. _V |-> ~P x ) , (/) ) )
9 5 8 mpbir
 |-  Lim dom R1
10 4 9 pm3.2i
 |-  ( Fun R1 /\ Lim dom R1 )