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 ⊢φ→MFnA×B
fnmpoovd.s ⊢i=a∧j=b→D=C
fnmpoovd.d ⊢φ∧i∈A∧j∈B→D∈U
fnmpoovd.c ⊢φ∧a∈A∧b∈B→C∈V
Assertion fnmpoovd ⊢φ→M=a∈A,b∈B⟼C↔∀i∈A∀j∈BiMj=D

Proof

Step Hyp Ref Expression
1 fnmpoovd.m ⊢φ→MFnA×B
2 fnmpoovd.s ⊢i=a∧j=b→D=C
3 fnmpoovd.d ⊢φ∧i∈A∧j∈B→D∈U
4 fnmpoovd.c ⊢φ∧a∈A∧b∈B→C∈V
5 4 3expb ⊢φ∧a∈A∧b∈B→C∈V
6 5 ralrimivva ⊢φ→∀a∈A∀b∈BC∈V
7 eqid ⊢a∈A,b∈B⟼C=a∈A,b∈B⟼C
8 7 fnmpo ⊢∀a∈A∀b∈BC∈V→a∈A,b∈B⟼CFnA×B
9 6 8 syl ⊢φ→a∈A,b∈B⟼CFnA×B
10 eqfnov2 ⊢MFnA×B∧a∈A,b∈B⟼CFnA×B→M=a∈A,b∈B⟼C↔∀i∈A∀j∈BiMj=ia∈A,b∈B⟼Cj
11 1 9 10 syl2anc ⊢φ→M=a∈A,b∈B⟼C↔∀i∈A∀j∈BiMj=ia∈A,b∈B⟼Cj
12 nfcv ⊢Ⅎ_aD
13 nfcv ⊢Ⅎ_bD
14 nfcv ⊢Ⅎ_iC
15 nfcv ⊢Ⅎ_jC
16 12 13 14 15 2 cbvmpo ⊢i∈A,j∈B⟼D=a∈A,b∈B⟼C
17 16 eqcomi ⊢a∈A,b∈B⟼C=i∈A,j∈B⟼D
18 17 a1i ⊢φ→a∈A,b∈B⟼C=i∈A,j∈B⟼D
19 18 oveqd ⊢φ→ia∈A,b∈B⟼Cj=ii∈A,j∈B⟼Dj
20 19 eqeq2d ⊢φ→iMj=ia∈A,b∈B⟼Cj↔iMj=ii∈A,j∈B⟼Dj
21 20 2ralbidv ⊢φ→∀i∈A∀j∈BiMj=ia∈A,b∈B⟼Cj↔∀i∈A∀j∈BiMj=ii∈A,j∈B⟼Dj
22 simprl ⊢φ∧i∈A∧j∈B→i∈A
23 simprr ⊢φ∧i∈A∧j∈B→j∈B
24 3 3expb ⊢φ∧i∈A∧j∈B→D∈U
25 eqid ⊢i∈A,j∈B⟼D=i∈A,j∈B⟼D
26 25 ovmpt4g ⊢i∈A∧j∈B∧D∈U→ii∈A,j∈B⟼Dj=D
27 22 23 24 26 syl3anc ⊢φ∧i∈A∧j∈B→ii∈A,j∈B⟼Dj=D
28 27 eqeq2d ⊢φ∧i∈A∧j∈B→iMj=ii∈A,j∈B⟼Dj↔iMj=D
29 28 2ralbidva ⊢φ→∀i∈A∀j∈BiMj=ii∈A,j∈B⟼Dj↔∀i∈A∀j∈BiMj=D
30 11 21 29 3bitrd ⊢φ→M=a∈A,b∈B⟼C↔∀i∈A∀j∈BiMj=D