Theorem r1elss

Description: The range of the R1 function is transitive. Lemma 2.10 of Kunen p. 97. (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Hypothesis	r1elss.1	|- A e. _V
Assertion	r1elss	|- ( A e. U. ( R1 " On ) <-> A C_ U. ( R1 " On ) )

Proof

Step	Hyp	Ref	Expression
1		r1elss.1	|- A e. _V
2		r1elssi	|- ( A e. U. ( R1 " On ) -> A C_ U. ( R1 " On ) )
3	1	tz9.12	|- ( A. y e. A E. x e. On y e. ( R1 ` x ) -> E. x e. On A e. ( R1 ` x ) )
4		dfss3	|- ( A C_ U. ( R1 " On ) <-> A. y e. A y e. U. ( R1 " On ) )
5		r1fnon	|- R1 Fn On
6		fnfun	|- ( R1 Fn On -> Fun R1 )
7		funiunfv	|- ( Fun R1 -> U_ x e. On ( R1 ` x ) = U. ( R1 " On ) )
8	5 6 7	mp2b	|- U_ x e. On ( R1 ` x ) = U. ( R1 " On )
9	8	eleq2i	|- ( y e. U_ x e. On ( R1 ` x ) <-> y e. U. ( R1 " On ) )
10		eliun	|- ( y e. U_ x e. On ( R1 ` x ) <-> E. x e. On y e. ( R1 ` x ) )
11	9 10	bitr3i	|- ( y e. U. ( R1 " On ) <-> E. x e. On y e. ( R1 ` x ) )
12	11	ralbii	|- ( A. y e. A y e. U. ( R1 " On ) <-> A. y e. A E. x e. On y e. ( R1 ` x ) )
13	4 12	bitri	|- ( A C_ U. ( R1 " On ) <-> A. y e. A E. x e. On y e. ( R1 ` x ) )
14	8	eleq2i	|- ( A e. U_ x e. On ( R1 ` x ) <-> A e. U. ( R1 " On ) )
15		eliun	|- ( A e. U_ x e. On ( R1 ` x ) <-> E. x e. On A e. ( R1 ` x ) )
16	14 15	bitr3i	|- ( A e. U. ( R1 " On ) <-> E. x e. On A e. ( R1 ` x ) )
17	3 13 16	3imtr4i	|- ( A C_ U. ( R1 " On ) -> A e. U. ( R1 " On ) )
18	2 17	impbii	|- ( A e. U. ( R1 " On ) <-> A C_ U. ( R1 " On ) )