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 )