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

Metamath Proof Explorer

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