Metamath Proof Explorer

Theorem wfgru

Description: The wellfounded part of a universe is another universe. (Contributed by Mario Carneiro, 17-Jun-2013)

Ref Expression
Assertion wfgru 
|- ( U e. Univ -> ( U i^i U. ( R1 " On ) ) e. Univ )

Proof

Step Hyp Ref Expression
1 dftr3 
 |-  ( Tr U. ( R1 " On ) <-> A. x e. U. ( R1 " On ) x C_ U. ( R1 " On ) )
2 r1elssi 
 |-  ( x e. U. ( R1 " On ) -> x C_ U. ( R1 " On ) )
3 1 2 mprgbir 
 |-  Tr U. ( R1 " On )
4 pwwf 
 |-  ( x e. U. ( R1 " On ) <-> ~P x e. U. ( R1 " On ) )
5 4 biimpi 
 |-  ( x e. U. ( R1 " On ) -> ~P x e. U. ( R1 " On ) )
6 prwf 
 |-  ( ( x e. U. ( R1 " On ) /\ y e. U. ( R1 " On ) ) -> { x , y } e. U. ( R1 " On ) )
7 6 ralrimiva 
 |-  ( x e. U. ( R1 " On ) -> A. y e. U. ( R1 " On ) { x , y } e. U. ( R1 " On ) )
8 frn 
 |-  ( y : x --> U. ( R1 " On ) -> ran y C_ U. ( R1 " On ) )
9 vex 
 |-  y e. _V
10 9 rnex 
 |-  ran y e. _V
11 10 r1elss 
 |-  ( ran y e. U. ( R1 " On ) <-> ran y C_ U. ( R1 " On ) )
12 uniwf 
 |-  ( ran y e. U. ( R1 " On ) <-> U. ran y e. U. ( R1 " On ) )
13 11 12 bitr3i 
 |-  ( ran y C_ U. ( R1 " On ) <-> U. ran y e. U. ( R1 " On ) )
14 8 13 sylib 
 |-  ( y : x --> U. ( R1 " On ) -> U. ran y e. U. ( R1 " On ) )
15 14 ax-gen 
 |-  A. y ( y : x --> U. ( R1 " On ) -> U. ran y e. U. ( R1 " On ) )
16 15 a1i 
 |-  ( x e. U. ( R1 " On ) -> A. y ( y : x --> U. ( R1 " On ) -> U. ran y e. U. ( R1 " On ) ) )
17 5 7 16 3jca 
 |-  ( x e. U. ( R1 " On ) -> ( ~P x e. U. ( R1 " On ) /\ A. y e. U. ( R1 " On ) { x , y } e. U. ( R1 " On ) /\ A. y ( y : x --> U. ( R1 " On ) -> U. ran y e. U. ( R1 " On ) ) ) )
18 17 rgen 
 |-  A. x e. U. ( R1 " On ) ( ~P x e. U. ( R1 " On ) /\ A. y e. U. ( R1 " On ) { x , y } e. U. ( R1 " On ) /\ A. y ( y : x --> U. ( R1 " On ) -> U. ran y e. U. ( R1 " On ) ) )
19 ingru 
 |-  ( ( Tr U. ( R1 " On ) /\ A. x e. U. ( R1 " On ) ( ~P x e. U. ( R1 " On ) /\ A. y e. U. ( R1 " On ) { x , y } e. U. ( R1 " On ) /\ A. y ( y : x --> U. ( R1 " On ) -> U. ran y e. U. ( R1 " On ) ) ) ) -> ( U e. Univ -> ( U i^i U. ( R1 " On ) ) e. Univ ) )
20 3 18 19 mp2an 
 |-  ( U e. Univ -> ( U i^i U. ( R1 " On ) ) e. Univ )