Metamath Proof Explorer

Theorem gruima

Description: A Grothendieck universe contains image sets drawn from its members. (Contributed by Mario Carneiro, 9-Jun-2013)

Ref Expression
Assertion gruima ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) → ( 𝐴 ∈ 𝑈 → ( 𝐹 “ 𝐴 ) ∈ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 simpl2 ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → Fun 𝐹 )
2 funrel ⊢ ( Fun 𝐹 → Rel 𝐹 )
3 df-ima ⊢ ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ 𝐴 )
4 resres ⊢ ( ( 𝐹 ↾ dom 𝐹 ) ↾ 𝐴 ) = ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) )
5 resdm ⊢ ( Rel 𝐹 → ( 𝐹 ↾ dom 𝐹 ) = 𝐹 )
6 5 reseq1d ⊢ ( Rel 𝐹 → ( ( 𝐹 ↾ dom 𝐹 ) ↾ 𝐴 ) = ( 𝐹 ↾ 𝐴 ) )
7 4 6 eqtr3id ⊢ ( Rel 𝐹 → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) = ( 𝐹 ↾ 𝐴 ) )
8 7 rneqd ⊢ ( Rel 𝐹 → ran ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) = ran ( 𝐹 ↾ 𝐴 ) )
9 3 8 eqtr4id ⊢ ( Rel 𝐹 → ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) )
10 1 2 9 3syl ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝐹 “ 𝐴 ) = ran ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) )
11 simpl1 ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → 𝑈 ∈ Univ )
12 simpr ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ∈ 𝑈 )
13 inss2 ⊢ ( dom 𝐹 ∩ 𝐴 ) ⊆ 𝐴
14 13 a1i ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → ( dom 𝐹 ∩ 𝐴 ) ⊆ 𝐴 )
15 gruss ⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ( dom 𝐹 ∩ 𝐴 ) ⊆ 𝐴 ) → ( dom 𝐹 ∩ 𝐴 ) ∈ 𝑈 )
16 11 12 14 15 syl3anc ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → ( dom 𝐹 ∩ 𝐴 ) ∈ 𝑈 )
17 funforn ⊢ ( Fun 𝐹 ↔ 𝐹 : dom 𝐹 –onto→ ran 𝐹 )
18 fof ⊢ ( 𝐹 : dom 𝐹 –onto→ ran 𝐹 → 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
19 17 18 sylbi ⊢ ( Fun 𝐹 → 𝐹 : dom 𝐹 ⟶ ran 𝐹 )
20 inss1 ⊢ ( dom 𝐹 ∩ 𝐴 ) ⊆ dom 𝐹
21 fssres ⊢ ( ( 𝐹 : dom 𝐹 ⟶ ran 𝐹 ∧ ( dom 𝐹 ∩ 𝐴 ) ⊆ dom 𝐹 ) → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ran 𝐹 )
22 19 20 21 sylancl ⊢ ( Fun 𝐹 → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ran 𝐹 )
23 ffn ⊢ ( ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ ran 𝐹 → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) Fn ( dom 𝐹 ∩ 𝐴 ) )
24 1 22 23 3syl ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) Fn ( dom 𝐹 ∩ 𝐴 ) )
25 simpl3 ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝐹 “ 𝐴 ) ⊆ 𝑈 )
26 10 25 eqsstrrd ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → ran ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) ⊆ 𝑈 )
27 df-f ⊢ ( ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ 𝑈 ↔ ( ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) Fn ( dom 𝐹 ∩ 𝐴 ) ∧ ran ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) ⊆ 𝑈 ) )
28 24 26 27 sylanbrc ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ 𝑈 )
29 grurn ⊢ ( ( 𝑈 ∈ Univ ∧ ( dom 𝐹 ∩ 𝐴 ) ∈ 𝑈 ∧ ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) : ( dom 𝐹 ∩ 𝐴 ) ⟶ 𝑈 ) → ran ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) ∈ 𝑈 )
30 11 16 28 29 syl3anc ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → ran ( 𝐹 ↾ ( dom 𝐹 ∩ 𝐴 ) ) ∈ 𝑈 )
31 10 30 eqeltrd ⊢ ( ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) ∧ 𝐴 ∈ 𝑈 ) → ( 𝐹 “ 𝐴 ) ∈ 𝑈 )
32 31 ex ⊢ ( ( 𝑈 ∈ Univ ∧ Fun 𝐹 ∧ ( 𝐹 “ 𝐴 ) ⊆ 𝑈 ) → ( 𝐴 ∈ 𝑈 → ( 𝐹 “ 𝐴 ) ∈ 𝑈 ) )