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 )