Theorem grurn

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	grurn	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → ran 𝐹 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → 𝑈 ∈ Univ )
2		gruurn	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → ∪ ran 𝐹 ∈ 𝑈 )
3		grupw	⊢ ( ( 𝑈 ∈ Univ ∧ ∪ ran 𝐹 ∈ 𝑈 ) → 𝒫 ∪ ran 𝐹 ∈ 𝑈 )
4	1 2 3	syl2anc	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → 𝒫 ∪ ran 𝐹 ∈ 𝑈 )
5		pwuni	⊢ ran 𝐹 ⊆ 𝒫 ∪ ran 𝐹
6	5	a1i	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → ran 𝐹 ⊆ 𝒫 ∪ ran 𝐹 )
7		gruss	⊢ ( ( 𝑈 ∈ Univ ∧ 𝒫 ∪ ran 𝐹 ∈ 𝑈 ∧ ran 𝐹 ⊆ 𝒫 ∪ ran 𝐹 ) → ran 𝐹 ∈ 𝑈 )
8	1 4 6 7	syl3anc	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → ran 𝐹 ∈ 𝑈 )