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 
|- ( ph -> M Fn ( A X. B ) )
fnmpoovd.s 
|- ( ( i = a /\ j = b ) -> D = C )
fnmpoovd.d 
|- ( ( ph /\ i e. A /\ j e. B ) -> D e. U )
fnmpoovd.c 
|- ( ( ph /\ a e. A /\ b e. B ) -> C e. V )
Assertion fnmpoovd 
|- ( ph -> ( M = ( a e. A , b e. B |-> C ) <-> A. i e. A A. j e. B ( i M j ) = D ) )

Proof

Step Hyp Ref Expression
1 fnmpoovd.m 
 |-  ( ph -> M Fn ( A X. B ) )
2 fnmpoovd.s 
 |-  ( ( i = a /\ j = b ) -> D = C )
3 fnmpoovd.d 
 |-  ( ( ph /\ i e. A /\ j e. B ) -> D e. U )
4 fnmpoovd.c 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> C e. V )
5 4 3expb 
 |-  ( ( ph /\ ( a e. A /\ b e. B ) ) -> C e. V )
6 5 ralrimivva 
 |-  ( ph -> A. a e. A A. b e. B C e. V )
7 eqid 
 |-  ( a e. A , b e. B |-> C ) = ( a e. A , b e. B |-> C )
8 7 fnmpo 
 |-  ( A. a e. A A. b e. B C e. V -> ( a e. A , b e. B |-> C ) Fn ( A X. B ) )
9 6 8 syl 
 |-  ( ph -> ( a e. A , b e. B |-> C ) Fn ( A X. B ) )
10 eqfnov2 
 |-  ( ( M Fn ( A X. B ) /\ ( a e. A , b e. B |-> C ) Fn ( A X. B ) ) -> ( M = ( a e. A , b e. B |-> C ) <-> A. i e. A A. j e. B ( i M j ) = ( i ( a e. A , b e. B |-> C ) j ) ) )
11 1 9 10 syl2anc 
 |-  ( ph -> ( M = ( a e. A , b e. B |-> C ) <-> A. i e. A A. j e. B ( i M j ) = ( i ( a e. A , b e. B |-> C ) j ) ) )
12 nfcv 
 |-  F/_ a D
13 nfcv 
 |-  F/_ b D
14 nfcv 
 |-  F/_ i C
15 nfcv 
 |-  F/_ j C
16 12 13 14 15 2 cbvmpo 
 |-  ( i e. A , j e. B |-> D ) = ( a e. A , b e. B |-> C )
17 16 eqcomi 
 |-  ( a e. A , b e. B |-> C ) = ( i e. A , j e. B |-> D )
18 17 a1i 
 |-  ( ph -> ( a e. A , b e. B |-> C ) = ( i e. A , j e. B |-> D ) )
19 18 oveqd 
 |-  ( ph -> ( i ( a e. A , b e. B |-> C ) j ) = ( i ( i e. A , j e. B |-> D ) j ) )
20 19 eqeq2d 
 |-  ( ph -> ( ( i M j ) = ( i ( a e. A , b e. B |-> C ) j ) <-> ( i M j ) = ( i ( i e. A , j e. B |-> D ) j ) ) )
21 20 2ralbidv 
 |-  ( ph -> ( A. i e. A A. j e. B ( i M j ) = ( i ( a e. A , b e. B |-> C ) j ) <-> A. i e. A A. j e. B ( i M j ) = ( i ( i e. A , j e. B |-> D ) j ) ) )
22 simprl 
 |-  ( ( ph /\ ( i e. A /\ j e. B ) ) -> i e. A )
23 simprr 
 |-  ( ( ph /\ ( i e. A /\ j e. B ) ) -> j e. B )
24 3 3expb 
 |-  ( ( ph /\ ( i e. A /\ j e. B ) ) -> D e. U )
25 eqid 
 |-  ( i e. A , j e. B |-> D ) = ( i e. A , j e. B |-> D )
26 25 ovmpt4g 
 |-  ( ( i e. A /\ j e. B /\ D e. U ) -> ( i ( i e. A , j e. B |-> D ) j ) = D )
27 22 23 24 26 syl3anc 
 |-  ( ( ph /\ ( i e. A /\ j e. B ) ) -> ( i ( i e. A , j e. B |-> D ) j ) = D )
28 27 eqeq2d 
 |-  ( ( ph /\ ( i e. A /\ j e. B ) ) -> ( ( i M j ) = ( i ( i e. A , j e. B |-> D ) j ) <-> ( i M j ) = D ) )
29 28 2ralbidva 
 |-  ( ph -> ( A. i e. A A. j e. B ( i M j ) = ( i ( i e. A , j e. B |-> D ) j ) <-> A. i e. A A. j e. B ( i M j ) = D ) )
30 11 21 29 3bitrd 
 |-  ( ph -> ( M = ( a e. A , b e. B |-> C ) <-> A. i e. A A. j e. B ( i M j ) = D ) )