Metamath Proof Explorer

Theorem gruurn

Description: A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013)

Ref Expression
Assertion gruurn ⊢ U ∈ Univ ∧ A ∈ U ∧ F : A ⟶ U → ⋃ ran ⁡ F ∈ U

Proof

Step Hyp Ref Expression
1 elmapg ⊢ U ∈ Univ ∧ A ∈ U → F ∈ U A ↔ F : A ⟶ U
2 elgrug ⊢ U ∈ Univ → U ∈ Univ ↔ Tr ⁡ U ∧ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
3 2 ibi ⊢ U ∈ Univ → Tr ⁡ U ∧ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
4 3 simprd ⊢ U ∈ Univ → ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U
5 rneq ⊢ y = F → ran ⁡ y = ran ⁡ F
6 5 unieqd ⊢ y = F → ⋃ ran ⁡ y = ⋃ ran ⁡ F
7 6 eleq1d ⊢ y = F → ⋃ ran ⁡ y ∈ U ↔ ⋃ ran ⁡ F ∈ U
8 7 rspccv ⊢ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U → F ∈ U x → ⋃ ran ⁡ F ∈ U
9 8 3ad2ant3 ⊢ 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U → F ∈ U x → ⋃ ran ⁡ F ∈ U
10 9 ralimi ⊢ ∀ x ∈ U 𝒫 x ∈ U ∧ ∀ y ∈ U x y ∈ U ∧ ∀ y ∈ U x ⋃ ran ⁡ y ∈ U → ∀ x ∈ U F ∈ U x → ⋃ ran ⁡ F ∈ U
11 oveq2 ⊢ x = A → U x = U A
12 11 eleq2d ⊢ x = A → F ∈ U x ↔ F ∈ U A
13 12 imbi1d ⊢ x = A → F ∈ U x → ⋃ ran ⁡ F ∈ U ↔ F ∈ U A → ⋃ ran ⁡ F ∈ U
14 13 rspccv ⊢ ∀ x ∈ U F ∈ U x → ⋃ ran ⁡ F ∈ U → A ∈ U → F ∈ U A → ⋃ ran ⁡ F ∈ U
15 4 10 14 3syl ⊢ U ∈ Univ → A ∈ U → F ∈ U A → ⋃ ran ⁡ F ∈ U
16 15 imp ⊢ U ∈ Univ ∧ A ∈ U → F ∈ U A → ⋃ ran ⁡ F ∈ U
17 1 16 sylbird ⊢ U ∈ Univ ∧ A ∈ U → F : A ⟶ U → ⋃ ran ⁡ F ∈ U
18 17 3impia ⊢ U ∈ Univ ∧ A ∈ U ∧ F : A ⟶ U → ⋃ ran ⁡ F ∈ U