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 ) = (/) )