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 
|- ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) -> ( A e. U -> ( F " A ) e. U ) )

Proof

Step Hyp Ref Expression
1 simpl2 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> Fun F )
2 funrel 
 |-  ( Fun F -> Rel F )
3 df-ima 
 |-  ( F " A ) = ran ( F |` A )
4 resres 
 |-  ( ( F |` dom F ) |` A ) = ( F |` ( dom F i^i A ) )
5 resdm 
 |-  ( Rel F -> ( F |` dom F ) = F )
6 5 reseq1d 
 |-  ( Rel F -> ( ( F |` dom F ) |` A ) = ( F |` A ) )
7 4 6 eqtr3id 
 |-  ( Rel F -> ( F |` ( dom F i^i A ) ) = ( F |` A ) )
8 7 rneqd 
 |-  ( Rel F -> ran ( F |` ( dom F i^i A ) ) = ran ( F |` A ) )
9 3 8 eqtr4id 
 |-  ( Rel F -> ( F " A ) = ran ( F |` ( dom F i^i A ) ) )
10 1 2 9 3syl 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> ( F " A ) = ran ( F |` ( dom F i^i A ) ) )
11 simpl1 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> U e. Univ )
12 simpr 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> A e. U )
13 inss2 
 |-  ( dom F i^i A ) C_ A
14 13 a1i 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> ( dom F i^i A ) C_ A )
15 gruss 
 |-  ( ( U e. Univ /\ A e. U /\ ( dom F i^i A ) C_ A ) -> ( dom F i^i A ) e. U )
16 11 12 14 15 syl3anc 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> ( dom F i^i A ) e. U )
17 funforn 
 |-  ( Fun F <-> F : dom F -onto-> ran F )
18 fof 
 |-  ( F : dom F -onto-> ran F -> F : dom F --> ran F )
19 17 18 sylbi 
 |-  ( Fun F -> F : dom F --> ran F )
20 inss1 
 |-  ( dom F i^i A ) C_ dom F
21 fssres 
 |-  ( ( F : dom F --> ran F /\ ( dom F i^i A ) C_ dom F ) -> ( F |` ( dom F i^i A ) ) : ( dom F i^i A ) --> ran F )
22 19 20 21 sylancl 
 |-  ( Fun F -> ( F |` ( dom F i^i A ) ) : ( dom F i^i A ) --> ran F )
23 ffn 
 |-  ( ( F |` ( dom F i^i A ) ) : ( dom F i^i A ) --> ran F -> ( F |` ( dom F i^i A ) ) Fn ( dom F i^i A ) )
24 1 22 23 3syl 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> ( F |` ( dom F i^i A ) ) Fn ( dom F i^i A ) )
25 simpl3 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> ( F " A ) C_ U )
26 10 25 eqsstrrd 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> ran ( F |` ( dom F i^i A ) ) C_ U )
27 df-f 
 |-  ( ( F |` ( dom F i^i A ) ) : ( dom F i^i A ) --> U <-> ( ( F |` ( dom F i^i A ) ) Fn ( dom F i^i A ) /\ ran ( F |` ( dom F i^i A ) ) C_ U ) )
28 24 26 27 sylanbrc 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> ( F |` ( dom F i^i A ) ) : ( dom F i^i A ) --> U )
29 grurn 
 |-  ( ( U e. Univ /\ ( dom F i^i A ) e. U /\ ( F |` ( dom F i^i A ) ) : ( dom F i^i A ) --> U ) -> ran ( F |` ( dom F i^i A ) ) e. U )
30 11 16 28 29 syl3anc 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> ran ( F |` ( dom F i^i A ) ) e. U )
31 10 30 eqeltrd 
 |-  ( ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) /\ A e. U ) -> ( F " A ) e. U )
32 31 ex 
 |-  ( ( U e. Univ /\ Fun F /\ ( F " A ) C_ U ) -> ( A e. U -> ( F " A ) e. U ) )