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

Metamath Proof Explorer

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 ) )