Metamath Proof Explorer

Theorem fnmpoovd

Description: A function with a Cartesian product as domain is a mapping with two arguments defined by its operation values. (Contributed by AV, 20-Feb-2019) (Revised by AV, 3-Jul-2022)

Ref Expression
Hypotheses fnmpoovd.m ⊢ ( 𝜑 → 𝑀 Fn ( 𝐴 × 𝐵 ) )
fnmpoovd.s ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → 𝐷 = 𝐶 )
fnmpoovd.d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) → 𝐷 ∈ 𝑈 )
fnmpoovd.c ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
Assertion fnmpoovd ( 𝜑 → ( 𝑀 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐵 ( 𝑖 𝑀 𝑗 ) = 𝐷 ) )

Proof

Step Hyp Ref Expression
1 fnmpoovd.m ⊢ ( 𝜑 → 𝑀 Fn ( 𝐴 × 𝐵 ) )
2 fnmpoovd.s ⊢ ( ( 𝑖 = 𝑎 ∧ 𝑗 = 𝑏 ) → 𝐷 = 𝐶 )
3 fnmpoovd.d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) → 𝐷 ∈ 𝑈 )
4 fnmpoovd.c ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
5 4 3expb ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → 𝐶 ∈ 𝑉 )
6 5 ralrimivva ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝐶 ∈ 𝑉 )
7 eqid ⊢ ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 )
8 7 fnmpo ⊢ ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 𝐶 ∈ 𝑉 → ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) Fn ( 𝐴 × 𝐵 ) )
9 6 8 syl ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) Fn ( 𝐴 × 𝐵 ) )
10 eqfnov2 ⊢ ( ( 𝑀 Fn ( 𝐴 × 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) Fn ( 𝐴 × 𝐵 ) ) → ( 𝑀 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐵 ( 𝑖 𝑀 𝑗 ) = ( 𝑖 ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) 𝑗 ) ) )
11 1 9 10 syl2anc ⊢ ( 𝜑 → ( 𝑀 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐵 ( 𝑖 𝑀 𝑗 ) = ( 𝑖 ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) 𝑗 ) ) )
12 nfcv ⊢ Ⅎ 𝑎 𝐷
13 nfcv ⊢ Ⅎ 𝑏 𝐷
14 nfcv ⊢ Ⅎ 𝑖 𝐶
15 nfcv ⊢ Ⅎ 𝑗 𝐶
16 12 13 14 15 2 cbvmpo ⊢ ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 ) = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 )
17 16 eqcomi ⊢ ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 )
18 17 a1i ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 ) )
19 18 oveqd ⊢ ( 𝜑 → ( 𝑖 ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) 𝑗 ) = ( 𝑖 ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 ) 𝑗 ) )
20 19 eqeq2d ⊢ ( 𝜑 → ( ( 𝑖 𝑀 𝑗 ) = ( 𝑖 ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) 𝑗 ) ↔ ( 𝑖 𝑀 𝑗 ) = ( 𝑖 ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 ) 𝑗 ) ) )
21 20 2ralbidv ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐵 ( 𝑖 𝑀 𝑗 ) = ( 𝑖 ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) 𝑗 ) ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐵 ( 𝑖 𝑀 𝑗 ) = ( 𝑖 ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 ) 𝑗 ) ) )
22 simprl ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑖 ∈ 𝐴 )
23 simprr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) → 𝑗 ∈ 𝐵 )
24 3 3expb ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) → 𝐷 ∈ 𝑈 )
25 eqid ⊢ ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 ) = ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 )
26 25 ovmpt4g ⊢ ( ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ∧ 𝐷 ∈ 𝑈 ) → ( 𝑖 ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 ) 𝑗 ) = 𝐷 )
27 22 23 24 26 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) → ( 𝑖 ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 ) 𝑗 ) = 𝐷 )
28 27 eqeq2d ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ 𝐴 ∧ 𝑗 ∈ 𝐵 ) ) → ( ( 𝑖 𝑀 𝑗 ) = ( 𝑖 ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 ) 𝑗 ) ↔ ( 𝑖 𝑀 𝑗 ) = 𝐷 ) )
29 28 2ralbidva ⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐵 ( 𝑖 𝑀 𝑗 ) = ( 𝑖 ( 𝑖 ∈ 𝐴 , 𝑗 ∈ 𝐵 ↦ 𝐷 ) 𝑗 ) ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐵 ( 𝑖 𝑀 𝑗 ) = 𝐷 ) )
30 11 21 29 3bitrd ⊢ ( 𝜑 → ( 𝑀 = ( 𝑎 ∈ 𝐴 , 𝑏 ∈ 𝐵 ↦ 𝐶 ) ↔ ∀ 𝑖 ∈ 𝐴 ∀ 𝑗 ∈ 𝐵 ( 𝑖 𝑀 𝑗 ) = 𝐷 ) )