This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )