Theorem r1elssi

Description: The range of the R1 function is transitive. Lemma 2.10 of Kunen p. 97. One direction of r1elss that doesn't need A to be a set. (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	r1elssi	|- ( A e. U. ( R1 " On ) -> A C_ U. ( R1 " On ) )

Proof

Step	Hyp	Ref	Expression
1		triun	|- ( A. x e. On Tr ( R1 ` x ) -> Tr U_ x e. On ( R1 ` x ) )
2		r1tr	|- Tr ( R1 ` x )
3	2	a1i	|- ( x e. On -> Tr ( R1 ` x ) )
4	1 3	mprg	|- Tr U_ x e. On ( R1 ` x )
5		r1funlim	|- ( Fun R1 /\ Lim dom R1 )
6	5	simpli	|- Fun R1
7		funiunfv	|- ( Fun R1 -> U_ x e. On ( R1 ` x ) = U. ( R1 " On ) )
8	6 7	ax-mp	|- U_ x e. On ( R1 ` x ) = U. ( R1 " On )
9		treq	|- ( U_ x e. On ( R1 ` x ) = U. ( R1 " On ) -> ( Tr U_ x e. On ( R1 ` x ) <-> Tr U. ( R1 " On ) ) )
10	8 9	ax-mp	|- ( Tr U_ x e. On ( R1 ` x ) <-> Tr U. ( R1 " On ) )
11	4 10	mpbi	|- Tr U. ( R1 " On )
12		trss	|- ( Tr U. ( R1 " On ) -> ( A e. U. ( R1 " On ) -> A C_ U. ( R1 " On ) ) )
13	11 12	ax-mp	|- ( A e. U. ( R1 " On ) -> A C_ U. ( R1 " On ) )