Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → ( 𝑀 = ( 𝑎 ∈ 𝐴 ↦ 𝐶 ) ↔ ∀ 𝑖 ∈ 𝐴 ( 𝑀 ‘ 𝑖 ) = 𝐷 ) )