Metamath Proof Explorer


Theorem rnmptssbi

Description: The range of an operation 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 ) )