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

Metamath Proof Explorer

Theorem jech9.3

Description: Every set belongs to some value of the cumulative hierarchy of sets function R1 , i.e. the indexed union of all values of R1 is the universe. Lemma 9.3 of Jech p. 71. (Contributed by NM, 4-Oct-2003) (Revised by Mario Carneiro, 8-Jun-2013)

Ref Expression
Assertion jech9.3 
|- U_ x e. On ( R1 ` x ) = _V

Proof

Step Hyp Ref Expression
1 r1fnon 
 |-  R1 Fn On
2 fniunfv 
 |-  ( R1 Fn On -> U_ x e. On ( R1 ` x ) = U. ran R1 )
3 1 2 ax-mp 
 |-  U_ x e. On ( R1 ` x ) = U. ran R1
4 fndm 
 |-  ( R1 Fn On -> dom R1 = On )
5 1 4 ax-mp 
 |-  dom R1 = On
6 5 imaeq2i 
 |-  ( R1 " dom R1 ) = ( R1 " On )
7 imadmrn 
 |-  ( R1 " dom R1 ) = ran R1
8 6 7 eqtr3i 
 |-  ( R1 " On ) = ran R1
9 8 unieqi 
 |-  U. ( R1 " On ) = U. ran R1
10 unir1 
 |-  U. ( R1 " On ) = _V
11 3 9 10 3eqtr2i 
 |-  U_ x e. On ( R1 ` x ) = _V