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

Proof

Step	Hyp	Ref	Expression
1		elmapg	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ( 𝐹 ∈ ( 𝑈 ↑m 𝐴 ) ↔ 𝐹 : 𝐴 ⟶ 𝑈 ) )
2		elgrug	⊢ ( 𝑈 ∈ Univ → ( 𝑈 ∈ Univ ↔ ( Tr 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) ) ) )
3	2	ibi	⊢ ( 𝑈 ∈ Univ → ( Tr 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) ) )
4	3	simprd	⊢ ( 𝑈 ∈ Univ → ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) )
5		rneq	⊢ ( 𝑦 = 𝐹 → ran 𝑦 = ran 𝐹 )
6	5	unieqd	⊢ ( 𝑦 = 𝐹 → ∪ ran 𝑦 = ∪ ran 𝐹 )
7	6	eleq1d	⊢ ( 𝑦 = 𝐹 → ( ∪ ran 𝑦 ∈ 𝑈 ↔ ∪ ran 𝐹 ∈ 𝑈 ) )
8	7	rspccv	⊢ ( ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 → ( 𝐹 ∈ ( 𝑈 ↑m 𝑥 ) → ∪ ran 𝐹 ∈ 𝑈 ) )
9	8	3ad2ant3	⊢ ( ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) → ( 𝐹 ∈ ( 𝑈 ↑m 𝑥 ) → ∪ ran 𝐹 ∈ 𝑈 ) )
10	9	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝑈 ( 𝐹 ∈ ( 𝑈 ↑m 𝑥 ) → ∪ ran 𝐹 ∈ 𝑈 ) )
11		oveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑈 ↑m 𝑥 ) = ( 𝑈 ↑m 𝐴 ) )
12	11	eleq2d	⊢ ( 𝑥 = 𝐴 → ( 𝐹 ∈ ( 𝑈 ↑m 𝑥 ) ↔ 𝐹 ∈ ( 𝑈 ↑m 𝐴 ) ) )
13	12	imbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ∈ ( 𝑈 ↑m 𝑥 ) → ∪ ran 𝐹 ∈ 𝑈 ) ↔ ( 𝐹 ∈ ( 𝑈 ↑m 𝐴 ) → ∪ ran 𝐹 ∈ 𝑈 ) ) )
14	13	rspccv	⊢ ( ∀ 𝑥 ∈ 𝑈 ( 𝐹 ∈ ( 𝑈 ↑m 𝑥 ) → ∪ ran 𝐹 ∈ 𝑈 ) → ( 𝐴 ∈ 𝑈 → ( 𝐹 ∈ ( 𝑈 ↑m 𝐴 ) → ∪ ran 𝐹 ∈ 𝑈 ) ) )
15	4 10 14	3syl	⊢ ( 𝑈 ∈ Univ → ( 𝐴 ∈ 𝑈 → ( 𝐹 ∈ ( 𝑈 ↑m 𝐴 ) → ∪ ran 𝐹 ∈ 𝑈 ) ) )
16	15	imp	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ( 𝐹 ∈ ( 𝑈 ↑m 𝐴 ) → ∪ ran 𝐹 ∈ 𝑈 ) )
17	1 16	sylbird	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ( 𝐹 : 𝐴 ⟶ 𝑈 → ∪ ran 𝐹 ∈ 𝑈 ) )
18	17	3impia	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → ∪ ran 𝐹 ∈ 𝑈 )