fnmptfvd

Description: A function with a given domain is a mapping defined by its function values. (Contributed by AV, 1-Mar-2019)

	Ref	Expression
Hypotheses	fnmptfvd.m	⊢ ( 𝜑 → 𝑀 Fn 𝐴 )
	fnmptfvd.s	⊢ ( 𝑖 = 𝑎 → 𝐷 = 𝐶 )
	fnmptfvd.d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝐷 ∈ 𝑈 )
	fnmptfvd.c	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
Assertion	fnmptfvd	⊢ ( 𝜑 → ( 𝑀 = ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) ↔ ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		fnmptfvd.m	⊢ ( 𝜑 → 𝑀 Fn 𝐴 )
2		fnmptfvd.s	⊢ ( 𝑖 = 𝑎 → 𝐷 = 𝐶 )
3		fnmptfvd.d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝐷 ∈ 𝑈 )
4		fnmptfvd.c	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
5	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 𝐶 ∈ 𝑉 )
6		eqid	⊢ ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑎 ∈ 𝐴 ↦ 𝐶 )
7	6	fnmpt	⊢ ( ∀ 𝑎 ∈ 𝐴 𝐶 ∈ 𝑉 → ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
8	5 7	syl	⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 )
9		eqfnfv	⊢ ( ( 𝑀 Fn 𝐴 ∧ ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) Fn 𝐴 ) → ( 𝑀 = ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) ↔ ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) = ( ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑖 ) ) )
10	1 8 9	syl2anc	⊢ ( 𝜑 → ( 𝑀 = ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) ↔ ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) = ( ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑖 ) ) )
11	2	cbvmptv	⊢ ( 𝑖 ∈ 𝐴 ↦ 𝐷 ) = ( 𝑎 ∈ 𝐴 ↦ 𝐶 )
12	11	eqcomi	⊢ ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑖 ∈ 𝐴 ↦ 𝐷 )
13	12	a1i	⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑖 ∈ 𝐴 ↦ 𝐷 ) )
14	13	fveq1d	⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑖 ) = ( ( 𝑖 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑖 ) )
15	14	eqeq2d	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝑖 ) = ( ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑖 ) ↔ ( 𝑀 ‘ 𝑖 ) = ( ( 𝑖 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑖 ) ) )
16	15	ralbidv	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) = ( ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) = ( ( 𝑖 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑖 ) ) )
17		simpr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → 𝑖 ∈ 𝐴 )
18		eqid	⊢ ( 𝑖 ∈ 𝐴 ↦ 𝐷 ) = ( 𝑖 ∈ 𝐴 ↦ 𝐷 )
19	18	fvmpt2	⊢ ( ( 𝑖 ∈ 𝐴 ∧ 𝐷 ∈ 𝑈 ) → ( ( 𝑖 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑖 ) = 𝐷 )
20	17 3 19	syl2anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( ( 𝑖 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑖 ) = 𝐷 )
21	20	eqeq2d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ) → ( ( 𝑀 ‘ 𝑖 ) = ( ( 𝑖 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑖 ) ↔ ( 𝑀 ‘ 𝑖 ) = 𝐷 ) )
22	21	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) = ( ( 𝑖 ∈ 𝐴 ↦ 𝐷 ) ‘ 𝑖 ) ↔ ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) = 𝐷 ) )
23	10 16 22	3bitrd	⊢ ( 𝜑 → ( 𝑀 = ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) ↔ ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) = 𝐷 ) )

Metamath Proof Explorer

Theorem fnmptfvd

Proof