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 ( 𝑈 ∈ Univ → ( 𝑈 ∩ ∪ ( 𝑅1 “ On ) ) ∈ Univ )

Proof

Step Hyp Ref Expression
1 dftr3 ⊢ ( Tr ∪ ( 𝑅1 “ On ) ↔ ∀ 𝑥 ∈ ∪ ( 𝑅1 “ On ) 𝑥 ⊆ ∪ ( 𝑅1 “ On ) )
2 r1elssi ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → 𝑥 ⊆ ∪ ( 𝑅1 “ On ) )
3 1 2 mprgbir ⊢ Tr ∪ ( 𝑅1 “ On )
4 pwwf ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ↔ 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
5 4 biimpi ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) )
6 prwf ⊢ ( ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) → { 𝑥 , 𝑦 } ∈ ∪ ( 𝑅1 “ On ) )
7 6 ralrimiva ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑦 ∈ ∪ ( 𝑅1 “ On ) { 𝑥 , 𝑦 } ∈ ∪ ( 𝑅1 “ On ) )
8 frn ⊢ ( 𝑦 : 𝑥 ⟶ ∪ ( 𝑅1 “ On ) → ran 𝑦 ⊆ ∪ ( 𝑅1 “ On ) )
9 vex ⊢ 𝑦 ∈ V
10 9 rnex ⊢ ran 𝑦 ∈ V
11 10 r1elss ⊢ ( ran 𝑦 ∈ ∪ ( 𝑅1 “ On ) ↔ ran 𝑦 ⊆ ∪ ( 𝑅1 “ On ) )
12 uniwf ⊢ ( ran 𝑦 ∈ ∪ ( 𝑅1 “ On ) ↔ ∪ ran 𝑦 ∈ ∪ ( 𝑅1 “ On ) )
13 11 12 bitr3i ⊢ ( ran 𝑦 ⊆ ∪ ( 𝑅1 “ On ) ↔ ∪ ran 𝑦 ∈ ∪ ( 𝑅1 “ On ) )
14 8 13 sylib ⊢ ( 𝑦 : 𝑥 ⟶ ∪ ( 𝑅1 “ On ) → ∪ ran 𝑦 ∈ ∪ ( 𝑅1 “ On ) )
15 14 ax-gen ⊢ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ ∪ ( 𝑅1 “ On ) → ∪ ran 𝑦 ∈ ∪ ( 𝑅1 “ On ) )
16 15 a1i ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ ∪ ( 𝑅1 “ On ) → ∪ ran 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
17 5 7 16 3jca ⊢ ( 𝑥 ∈ ∪ ( 𝑅1 “ On ) → ( 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ ∪ ( 𝑅1 “ On ) { 𝑥 , 𝑦 } ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ ∪ ( 𝑅1 “ On ) → ∪ ran 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) ) )
18 17 rgen ⊢ ∀ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ( 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ ∪ ( 𝑅1 “ On ) { 𝑥 , 𝑦 } ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ ∪ ( 𝑅1 “ On ) → ∪ ran 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) )
19 ingru ⊢ ( ( Tr ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑥 ∈ ∪ ( 𝑅1 “ On ) ( 𝒫 𝑥 ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ∈ ∪ ( 𝑅1 “ On ) { 𝑥 , 𝑦 } ∈ ∪ ( 𝑅1 “ On ) ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ ∪ ( 𝑅1 “ On ) → ∪ ran 𝑦 ∈ ∪ ( 𝑅1 “ On ) ) ) ) → ( 𝑈 ∈ Univ → ( 𝑈 ∩ ∪ ( 𝑅1 “ On ) ) ∈ Univ ) )
20 3 18 19 mp2an ⊢ ( 𝑈 ∈ Univ → ( 𝑈 ∩ ∪ ( 𝑅1 “ On ) ) ∈ Univ )