This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rnmptssbi

Description: The range of a function given by the maps-to notation as a subset. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses rnmptssbi.1 
|- F/ x ph
rnmptssbi.2 
|- F = ( x e. A |-> B )
rnmptssbi.3 
|- ( ( ph /\ x e. A ) -> B e. V )
Assertion rnmptssbi 
|- ( ph -> ( ran F C_ C <-> A. x e. A B e. C ) )

Proof

Step Hyp Ref Expression
1 rnmptssbi.1 
 |-  F/ x ph
2 rnmptssbi.2 
 |-  F = ( x e. A |-> B )
3 rnmptssbi.3 
 |-  ( ( ph /\ x e. A ) -> B e. V )
4 nfmpt1 
 |-  F/_ x ( x e. A |-> B )
5 2 4 nfcxfr 
 |-  F/_ x F
6 5 nfrn 
 |-  F/_ x ran F
7 nfcv 
 |-  F/_ x C
8 6 7 nfss 
 |-  F/ x ran F C_ C
9 1 8 nfan 
 |-  F/ x ( ph /\ ran F C_ C )
10 simplr 
 |-  ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> ran F C_ C )
11 simpr 
 |-  ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> x e. A )
12 3 adantlr 
 |-  ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> B e. V )
13 2 11 12 elrnmpt1d 
 |-  ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> B e. ran F )
14 10 13 sseldd 
 |-  ( ( ( ph /\ ran F C_ C ) /\ x e. A ) -> B e. C )
15 9 14 ralrimia 
 |-  ( ( ph /\ ran F C_ C ) -> A. x e. A B e. C )
16 2 rnmptss 
 |-  ( A. x e. A B e. C -> ran F C_ C )
17 16 adantl 
 |-  ( ( ph /\ A. x e. A B e. C ) -> ran F C_ C )
18 15 17 impbida 
 |-  ( ph -> ( ran F C_ C <-> A. x e. A B e. C ) )