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

Metamath Proof Explorer

Theorem fvmptnf

Description: The value of a function given by an ordered-pair class abstraction is the empty set when the class it would otherwise map to is a proper class. This version of fvmptn uses bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 21-Oct-2003) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses fvmptf.1 
|- F/_ x A
fvmptf.2 
|- F/_ x C
fvmptf.3 
|- ( x = A -> B = C )
fvmptf.4 
|- F = ( x e. D |-> B )
Assertion fvmptnf 
|- ( -. C e. _V -> ( F ` A ) = (/) )

Proof

Step Hyp Ref Expression
1 fvmptf.1 
 |-  F/_ x A
2 fvmptf.2 
 |-  F/_ x C
3 fvmptf.3 
 |-  ( x = A -> B = C )
4 fvmptf.4 
 |-  F = ( x e. D |-> B )
5 4 dmmptss 
 |-  dom F C_ D
6 5 sseli 
 |-  ( A e. dom F -> A e. D )
7 eqid 
 |-  ( x e. D |-> ( _I ` B ) ) = ( x e. D |-> ( _I ` B ) )
8 4 7 fvmptex 
 |-  ( F ` A ) = ( ( x e. D |-> ( _I ` B ) ) ` A )
9 fvex 
 |-  ( _I ` C ) e. _V
10 nfcv 
 |-  F/_ x _I
11 10 2 nffv 
 |-  F/_ x ( _I ` C )
12 3 fveq2d 
 |-  ( x = A -> ( _I ` B ) = ( _I ` C ) )
13 1 11 12 7 fvmptf 
 |-  ( ( A e. D /\ ( _I ` C ) e. _V ) -> ( ( x e. D |-> ( _I ` B ) ) ` A ) = ( _I ` C ) )
14 9 13 mpan2 
 |-  ( A e. D -> ( ( x e. D |-> ( _I ` B ) ) ` A ) = ( _I ` C ) )
15 8 14 eqtrid 
 |-  ( A e. D -> ( F ` A ) = ( _I ` C ) )
16 fvprc 
 |-  ( -. C e. _V -> ( _I ` C ) = (/) )
17 15 16 sylan9eq 
 |-  ( ( A e. D /\ -. C e. _V ) -> ( F ` A ) = (/) )
18 17 expcom 
 |-  ( -. C e. _V -> ( A e. D -> ( F ` A ) = (/) ) )
19 6 18 syl5 
 |-  ( -. C e. _V -> ( A e. dom F -> ( F ` A ) = (/) ) )
20 ndmfv 
 |-  ( -. A e. dom F -> ( F ` A ) = (/) )
21 19 20 pm2.61d1 
 |-  ( -. C e. _V -> ( F ` A ) = (/) )