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

Metamath Proof Explorer

Theorem fvmptex

Description: Express a function F whose value B may not always be a set in terms of another function G for which sethood is guaranteed. (Note that (IB ) is just shorthand for if ( B e. V , B , (/) ) , and it is always a set by fvex .) Note also that these functions are not the same; wherever B ( C ) is not a set, C is not in the domain of F (so it evaluates to the empty set), but C is in the domain of G , and G ( C ) is defined to be the empty set. (Contributed by Mario Carneiro, 14-Jul-2013) (Revised by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses fvmptex.1 
|- F = ( x e. A |-> B )
fvmptex.2 
|- G = ( x e. A |-> ( _I ` B ) )
Assertion fvmptex 
|- ( F ` C ) = ( G ` C )

Proof

Step Hyp Ref Expression
1 fvmptex.1 
 |-  F = ( x e. A |-> B )
2 fvmptex.2 
 |-  G = ( x e. A |-> ( _I ` B ) )
3 csbeq1 
 |-  ( y = C -> [_ y / x ]_ B = [_ C / x ]_ B )
4 nfcv 
 |-  F/_ y B
5 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
6 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
7 4 5 6 cbvmpt 
 |-  ( x e. A |-> B ) = ( y e. A |-> [_ y / x ]_ B )
8 1 7 eqtri 
 |-  F = ( y e. A |-> [_ y / x ]_ B )
9 3 8 fvmpti 
 |-  ( C e. A -> ( F ` C ) = ( _I ` [_ C / x ]_ B ) )
10 3 fveq2d 
 |-  ( y = C -> ( _I ` [_ y / x ]_ B ) = ( _I ` [_ C / x ]_ B ) )
11 nfcv 
 |-  F/_ y ( _I ` B )
12 nfcv 
 |-  F/_ x _I
13 12 5 nffv 
 |-  F/_ x ( _I ` [_ y / x ]_ B )
14 6 fveq2d 
 |-  ( x = y -> ( _I ` B ) = ( _I ` [_ y / x ]_ B ) )
15 11 13 14 cbvmpt 
 |-  ( x e. A |-> ( _I ` B ) ) = ( y e. A |-> ( _I ` [_ y / x ]_ B ) )
16 2 15 eqtri 
 |-  G = ( y e. A |-> ( _I ` [_ y / x ]_ B ) )
17 fvex 
 |-  ( _I ` [_ C / x ]_ B ) e. _V
18 10 16 17 fvmpt 
 |-  ( C e. A -> ( G ` C ) = ( _I ` [_ C / x ]_ B ) )
19 9 18 eqtr4d 
 |-  ( C e. A -> ( F ` C ) = ( G ` C ) )
20 1 dmmptss 
 |-  dom F C_ A
21 20 sseli 
 |-  ( C e. dom F -> C e. A )
22 ndmfv 
 |-  ( -. C e. dom F -> ( F ` C ) = (/) )
23 21 22 nsyl5 
 |-  ( -. C e. A -> ( F ` C ) = (/) )
24 fvex 
 |-  ( _I ` B ) e. _V
25 24 2 dmmpti 
 |-  dom G = A
26 25 eleq2i 
 |-  ( C e. dom G <-> C e. A )
27 ndmfv 
 |-  ( -. C e. dom G -> ( G ` C ) = (/) )
28 26 27 sylnbir 
 |-  ( -. C e. A -> ( G ` C ) = (/) )
29 23 28 eqtr4d 
 |-  ( -. C e. A -> ( F ` C ) = ( G ` C ) )
30 19 29 pm2.61i 
 |-  ( F ` C ) = ( G ` C )