Metamath Proof Explorer

Theorem fvmpopr2d

Description: Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024)

Ref Expression
Hypotheses fvmpopr2d.1 
|- ( ph -> F = ( a e. A , b e. B |-> C ) )
fvmpopr2d.2 
|- ( ph -> P = <. a , b >. )
fvmpopr2d.3 
|- ( ( ph /\ a e. A /\ b e. B ) -> C e. V )
Assertion fvmpopr2d 
|- ( ( ph /\ a e. A /\ b e. B ) -> ( F ` P ) = C )

Proof

Step Hyp Ref Expression
1 fvmpopr2d.1 
 |-  ( ph -> F = ( a e. A , b e. B |-> C ) )
2 fvmpopr2d.2 
 |-  ( ph -> P = <. a , b >. )
3 fvmpopr2d.3 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> C e. V )
4 df-ov 
 |-  ( a ( a e. A , b e. B |-> C ) b ) = ( ( a e. A , b e. B |-> C ) ` <. a , b >. )
5 1 3ad2ant1 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> F = ( a e. A , b e. B |-> C ) )
6 2 3ad2ant1 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> P = <. a , b >. )
7 5 6 fveq12d 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( F ` P ) = ( ( a e. A , b e. B |-> C ) ` <. a , b >. ) )
8 4 7 eqtr4id 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( a ( a e. A , b e. B |-> C ) b ) = ( F ` P ) )
9 nfcv 
 |-  F/_ c C
10 nfcv 
 |-  F/_ d C
11 nfcv 
 |-  F/_ a d
12 nfcsb1v 
 |-  F/_ a [_ c / a ]_ C
13 11 12 nfcsbw 
 |-  F/_ a [_ d / b ]_ [_ c / a ]_ C
14 nfcsb1v 
 |-  F/_ b [_ d / b ]_ [_ c / a ]_ C
15 csbeq1a 
 |-  ( a = c -> C = [_ c / a ]_ C )
16 csbeq1a 
 |-  ( b = d -> [_ c / a ]_ C = [_ d / b ]_ [_ c / a ]_ C )
17 15 16 sylan9eq 
 |-  ( ( a = c /\ b = d ) -> C = [_ d / b ]_ [_ c / a ]_ C )
18 9 10 13 14 17 cbvmpo 
 |-  ( a e. A , b e. B |-> C ) = ( c e. A , d e. B |-> [_ d / b ]_ [_ c / a ]_ C )
19 18 oveqi 
 |-  ( a ( a e. A , b e. B |-> C ) b ) = ( a ( c e. A , d e. B |-> [_ d / b ]_ [_ c / a ]_ C ) b )
20 eqidd 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( c e. A , d e. B |-> [_ d / b ]_ [_ c / a ]_ C ) = ( c e. A , d e. B |-> [_ d / b ]_ [_ c / a ]_ C ) )
21 equcom 
 |-  ( a = c <-> c = a )
22 equcom 
 |-  ( b = d <-> d = b )
23 21 22 anbi12i 
 |-  ( ( a = c /\ b = d ) <-> ( c = a /\ d = b ) )
24 23 17 sylbir 
 |-  ( ( c = a /\ d = b ) -> C = [_ d / b ]_ [_ c / a ]_ C )
25 24 eqcomd 
 |-  ( ( c = a /\ d = b ) -> [_ d / b ]_ [_ c / a ]_ C = C )
26 25 adantl 
 |-  ( ( ( ph /\ a e. A /\ b e. B ) /\ ( c = a /\ d = b ) ) -> [_ d / b ]_ [_ c / a ]_ C = C )
27 simp2 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> a e. A )
28 simp3 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> b e. B )
29 20 26 27 28 3 ovmpod 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( a ( c e. A , d e. B |-> [_ d / b ]_ [_ c / a ]_ C ) b ) = C )
30 19 29 eqtrid 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( a ( a e. A , b e. B |-> C ) b ) = C )
31 8 30 eqtr3d 
 |-  ( ( ph /\ a e. A /\ b e. B ) -> ( F ` P ) = C )