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	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	fvmptex.2	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( I ‘ 𝐵 ) )
Assertion	fvmptex	⊢ ( 𝐹 ‘ 𝐶 ) = ( 𝐺 ‘ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fvmptex.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		fvmptex.2	⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( I ‘ 𝐵 ) )
3		csbeq1	⊢ ( 𝑦 = 𝐶 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐶 / 𝑥 ⦌ 𝐵 )
4		nfcv	⊢ Ⅎ 𝑦 𝐵
5		nfcsb1v	⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
6		csbeq1a	⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
7	4 5 6	cbvmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
8	1 7	eqtri	⊢ 𝐹 = ( 𝑦 ∈ 𝐴 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
9	3 8	fvmpti	⊢ ( 𝐶 ∈ 𝐴 → ( 𝐹 ‘ 𝐶 ) = ( I ‘ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) )
10	3	fveq2d	⊢ ( 𝑦 = 𝐶 → ( I ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) = ( I ‘ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) )
11		nfcv	⊢ Ⅎ 𝑦 ( I ‘ 𝐵 )
12		nfcv	⊢ Ⅎ 𝑥 I
13	12 5	nffv	⊢ Ⅎ 𝑥 ( I ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
14	6	fveq2d	⊢ ( 𝑥 = 𝑦 → ( I ‘ 𝐵 ) = ( I ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
15	11 13 14	cbvmpt	⊢ ( 𝑥 ∈ 𝐴 ↦ ( I ‘ 𝐵 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( I ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
16	2 15	eqtri	⊢ 𝐺 = ( 𝑦 ∈ 𝐴 ↦ ( I ‘ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
17		fvex	⊢ ( I ‘ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) ∈ V
18	10 16 17	fvmpt	⊢ ( 𝐶 ∈ 𝐴 → ( 𝐺 ‘ 𝐶 ) = ( I ‘ ⦋ 𝐶 / 𝑥 ⦌ 𝐵 ) )
19	9 18	eqtr4d	⊢ ( 𝐶 ∈ 𝐴 → ( 𝐹 ‘ 𝐶 ) = ( 𝐺 ‘ 𝐶 ) )
20	1	dmmptss	⊢ dom 𝐹 ⊆ 𝐴
21	20	sseli	⊢ ( 𝐶 ∈ dom 𝐹 → 𝐶 ∈ 𝐴 )
22		ndmfv	⊢ ( ¬ 𝐶 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐶 ) = ∅ )
23	21 22	nsyl5	⊢ ( ¬ 𝐶 ∈ 𝐴 → ( 𝐹 ‘ 𝐶 ) = ∅ )
24		fvex	⊢ ( I ‘ 𝐵 ) ∈ V
25	24 2	dmmpti	⊢ dom 𝐺 = 𝐴
26	25	eleq2i	⊢ ( 𝐶 ∈ dom 𝐺 ↔ 𝐶 ∈ 𝐴 )
27		ndmfv	⊢ ( ¬ 𝐶 ∈ dom 𝐺 → ( 𝐺 ‘ 𝐶 ) = ∅ )
28	26 27	sylnbir	⊢ ( ¬ 𝐶 ∈ 𝐴 → ( 𝐺 ‘ 𝐶 ) = ∅ )
29	23 28	eqtr4d	⊢ ( ¬ 𝐶 ∈ 𝐴 → ( 𝐹 ‘ 𝐶 ) = ( 𝐺 ‘ 𝐶 ) )
30	19 29	pm2.61i	⊢ ( 𝐹 ‘ 𝐶 ) = ( 𝐺 ‘ 𝐶 )