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 Univ U R1 On Univ

Proof

Step Hyp Ref Expression
1 dftr3 Tr R1 On x R1 On x R1 On
2 r1elssi x R1 On x R1 On
3 1 2 mprgbir Tr R1 On
4 pwwf x R1 On 𝒫 x R1 On
5 4 biimpi x R1 On 𝒫 x R1 On
6 prwf x R1 On y R1 On x y R1 On
7 6 ralrimiva x R1 On y R1 On x y R1 On
8 frn y : x R1 On ran y R1 On
9 vex y V
10 9 rnex ran y V
11 10 r1elss ran y R1 On ran y R1 On
12 uniwf ran y R1 On ran y R1 On
13 11 12 bitr3i ran y R1 On ran y R1 On
14 8 13 sylib y : x R1 On ran y R1 On
15 14 ax-gen y y : x R1 On ran y R1 On
16 15 a1i x R1 On y y : x R1 On ran y R1 On
17 5 7 16 3jca x R1 On 𝒫 x R1 On y R1 On x y R1 On y y : x R1 On ran y R1 On
18 17 rgen x R1 On 𝒫 x R1 On y R1 On x y R1 On y y : x R1 On ran y R1 On
19 ingru Tr R1 On x R1 On 𝒫 x R1 On y R1 On x y R1 On y y : x R1 On ran y R1 On U Univ U R1 On Univ
20 3 18 19 mp2an U Univ U R1 On Univ