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

Metamath Proof Explorer

Theorem nelrnmpt

Description: Non-membership in the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses nelrnmpt.x 
|- F/ x ph
nelrnmpt.f 
|- F = ( x e. A |-> B )
nelrnmpt.c 
|- ( ph -> C e. V )
nelrnmpt.n 
|- ( ( ph /\ x e. A ) -> C =/= B )
Assertion nelrnmpt 
|- ( ph -> -. C e. ran F )

Proof

Step Hyp Ref Expression
1 nelrnmpt.x 
 |-  F/ x ph
2 nelrnmpt.f 
 |-  F = ( x e. A |-> B )
3 nelrnmpt.c 
 |-  ( ph -> C e. V )
4 nelrnmpt.n 
 |-  ( ( ph /\ x e. A ) -> C =/= B )
5 4 neneqd 
 |-  ( ( ph /\ x e. A ) -> -. C = B )
6 5 ex 
 |-  ( ph -> ( x e. A -> -. C = B ) )
7 1 6 ralrimi 
 |-  ( ph -> A. x e. A -. C = B )
8 ralnex 
 |-  ( A. x e. A -. C = B <-> -. E. x e. A C = B )
9 7 8 sylib 
 |-  ( ph -> -. E. x e. A C = B )
10 2 elrnmpt 
 |-  ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )
11 3 10 syl 
 |-  ( ph -> ( C e. ran F <-> E. x e. A C = B ) )
12 9 11 mtbird 
 |-  ( ph -> -. C e. ran F )