Metamath Proof Explorer

Theorem offval22

Description: The function operation expressed as a mapping, variation of offval2 . (Contributed by SO, 15-Jul-2018)

Ref Expression
Hypotheses offval22.a 
|- ( ph -> A e. V )
offval22.b 
|- ( ph -> B e. W )
offval22.c 
|- ( ( ph /\ x e. A /\ y e. B ) -> C e. X )
offval22.d 
|- ( ( ph /\ x e. A /\ y e. B ) -> D e. Y )
offval22.f 
|- ( ph -> F = ( x e. A , y e. B |-> C ) )
offval22.g 
|- ( ph -> G = ( x e. A , y e. B |-> D ) )
Assertion offval22 
|- ( ph -> ( F oF R G ) = ( x e. A , y e. B |-> ( C R D ) ) )

Proof

Step Hyp Ref Expression
1 offval22.a 
 |-  ( ph -> A e. V )
2 offval22.b 
 |-  ( ph -> B e. W )
3 offval22.c 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> C e. X )
4 offval22.d 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> D e. Y )
5 offval22.f 
 |-  ( ph -> F = ( x e. A , y e. B |-> C ) )
6 offval22.g 
 |-  ( ph -> G = ( x e. A , y e. B |-> D ) )
7 1 2 xpexd 
 |-  ( ph -> ( A X. B ) e. _V )
8 xp1st 
 |-  ( z e. ( A X. B ) -> ( 1st ` z ) e. A )
9 xp2nd 
 |-  ( z e. ( A X. B ) -> ( 2nd ` z ) e. B )
10 8 9 jca 
 |-  ( z e. ( A X. B ) -> ( ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) )
11 fvex 
 |-  ( 2nd ` z ) e. _V
12 fvex 
 |-  ( 1st ` z ) e. _V
13 nfcv 
 |-  F/_ y ( 2nd ` z )
14 nfcv 
 |-  F/_ x ( 2nd ` z )
15 nfcv 
 |-  F/_ x ( 1st ` z )
16 nfv 
 |-  F/ y ( ph /\ x e. A /\ ( 2nd ` z ) e. B )
17 nfcsb1v 
 |-  F/_ y [_ ( 2nd ` z ) / y ]_ C
18 17 nfel1 
 |-  F/ y [_ ( 2nd ` z ) / y ]_ C e. _V
19 16 18 nfim 
 |-  F/ y ( ( ph /\ x e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 2nd ` z ) / y ]_ C e. _V )
20 nfv 
 |-  F/ x ( ph /\ ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B )
21 nfcsb1v 
 |-  F/_ x [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C
22 21 nfel1 
 |-  F/ x [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C e. _V
23 20 22 nfim 
 |-  F/ x ( ( ph /\ ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C e. _V )
24 eleq1 
 |-  ( y = ( 2nd ` z ) -> ( y e. B <-> ( 2nd ` z ) e. B ) )
25 24 3anbi3d 
 |-  ( y = ( 2nd ` z ) -> ( ( ph /\ x e. A /\ y e. B ) <-> ( ph /\ x e. A /\ ( 2nd ` z ) e. B ) ) )
26 csbeq1a 
 |-  ( y = ( 2nd ` z ) -> C = [_ ( 2nd ` z ) / y ]_ C )
27 26 eleq1d 
 |-  ( y = ( 2nd ` z ) -> ( C e. _V <-> [_ ( 2nd ` z ) / y ]_ C e. _V ) )
28 25 27 imbi12d 
 |-  ( y = ( 2nd ` z ) -> ( ( ( ph /\ x e. A /\ y e. B ) -> C e. _V ) <-> ( ( ph /\ x e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 2nd ` z ) / y ]_ C e. _V ) ) )
29 eleq1 
 |-  ( x = ( 1st ` z ) -> ( x e. A <-> ( 1st ` z ) e. A ) )
30 29 3anbi2d 
 |-  ( x = ( 1st ` z ) -> ( ( ph /\ x e. A /\ ( 2nd ` z ) e. B ) <-> ( ph /\ ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) ) )
31 csbeq1a 
 |-  ( x = ( 1st ` z ) -> [_ ( 2nd ` z ) / y ]_ C = [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C )
32 31 eleq1d 
 |-  ( x = ( 1st ` z ) -> ( [_ ( 2nd ` z ) / y ]_ C e. _V <-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C e. _V ) )
33 30 32 imbi12d 
 |-  ( x = ( 1st ` z ) -> ( ( ( ph /\ x e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 2nd ` z ) / y ]_ C e. _V ) <-> ( ( ph /\ ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C e. _V ) ) )
34 3 elexd 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> C e. _V )
35 13 14 15 19 23 28 33 34 vtocl2gf 
 |-  ( ( ( 2nd ` z ) e. _V /\ ( 1st ` z ) e. _V ) -> ( ( ph /\ ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C e. _V ) )
36 11 12 35 mp2an 
 |-  ( ( ph /\ ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C e. _V )
37 36 3expb 
 |-  ( ( ph /\ ( ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C e. _V )
38 10 37 sylan2 
 |-  ( ( ph /\ z e. ( A X. B ) ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C e. _V )
39 nfcsb1v 
 |-  F/_ y [_ ( 2nd ` z ) / y ]_ D
40 39 nfel1 
 |-  F/ y [_ ( 2nd ` z ) / y ]_ D e. _V
41 16 40 nfim 
 |-  F/ y ( ( ph /\ x e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 2nd ` z ) / y ]_ D e. _V )
42 nfcsb1v 
 |-  F/_ x [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D
43 42 nfel1 
 |-  F/ x [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D e. _V
44 20 43 nfim 
 |-  F/ x ( ( ph /\ ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D e. _V )
45 csbeq1a 
 |-  ( y = ( 2nd ` z ) -> D = [_ ( 2nd ` z ) / y ]_ D )
46 45 eleq1d 
 |-  ( y = ( 2nd ` z ) -> ( D e. _V <-> [_ ( 2nd ` z ) / y ]_ D e. _V ) )
47 25 46 imbi12d 
 |-  ( y = ( 2nd ` z ) -> ( ( ( ph /\ x e. A /\ y e. B ) -> D e. _V ) <-> ( ( ph /\ x e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 2nd ` z ) / y ]_ D e. _V ) ) )
48 csbeq1a 
 |-  ( x = ( 1st ` z ) -> [_ ( 2nd ` z ) / y ]_ D = [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D )
49 48 eleq1d 
 |-  ( x = ( 1st ` z ) -> ( [_ ( 2nd ` z ) / y ]_ D e. _V <-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D e. _V ) )
50 30 49 imbi12d 
 |-  ( x = ( 1st ` z ) -> ( ( ( ph /\ x e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 2nd ` z ) / y ]_ D e. _V ) <-> ( ( ph /\ ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D e. _V ) ) )
51 4 elexd 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> D e. _V )
52 13 14 15 41 44 47 50 51 vtocl2gf 
 |-  ( ( ( 2nd ` z ) e. _V /\ ( 1st ` z ) e. _V ) -> ( ( ph /\ ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D e. _V ) )
53 11 12 52 mp2an 
 |-  ( ( ph /\ ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D e. _V )
54 53 3expb 
 |-  ( ( ph /\ ( ( 1st ` z ) e. A /\ ( 2nd ` z ) e. B ) ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D e. _V )
55 10 54 sylan2 
 |-  ( ( ph /\ z e. ( A X. B ) ) -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D e. _V )
56 mpompts 
 |-  ( x e. A , y e. B |-> C ) = ( z e. ( A X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C )
57 5 56 eqtrdi 
 |-  ( ph -> F = ( z e. ( A X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C ) )
58 mpompts 
 |-  ( x e. A , y e. B |-> D ) = ( z e. ( A X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D )
59 6 58 eqtrdi 
 |-  ( ph -> G = ( z e. ( A X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D ) )
60 7 38 55 57 59 offval2 
 |-  ( ph -> ( F oF R G ) = ( z e. ( A X. B ) |-> ( [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C R [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D ) ) )
61 csbov12g 
 |-  ( ( 2nd ` z ) e. _V -> [_ ( 2nd ` z ) / y ]_ ( C R D ) = ( [_ ( 2nd ` z ) / y ]_ C R [_ ( 2nd ` z ) / y ]_ D ) )
62 61 csbeq2dv 
 |-  ( ( 2nd ` z ) e. _V -> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ ( C R D ) = [_ ( 1st ` z ) / x ]_ ( [_ ( 2nd ` z ) / y ]_ C R [_ ( 2nd ` z ) / y ]_ D ) )
63 11 62 ax-mp 
 |-  [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ ( C R D ) = [_ ( 1st ` z ) / x ]_ ( [_ ( 2nd ` z ) / y ]_ C R [_ ( 2nd ` z ) / y ]_ D )
64 csbov12g 
 |-  ( ( 1st ` z ) e. _V -> [_ ( 1st ` z ) / x ]_ ( [_ ( 2nd ` z ) / y ]_ C R [_ ( 2nd ` z ) / y ]_ D ) = ( [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C R [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D ) )
65 12 64 ax-mp 
 |-  [_ ( 1st ` z ) / x ]_ ( [_ ( 2nd ` z ) / y ]_ C R [_ ( 2nd ` z ) / y ]_ D ) = ( [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C R [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D )
66 63 65 eqtr2i 
 |-  ( [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C R [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D ) = [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ ( C R D )
67 66 mpteq2i 
 |-  ( z e. ( A X. B ) |-> ( [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C R [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D ) ) = ( z e. ( A X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ ( C R D ) )
68 mpompts 
 |-  ( x e. A , y e. B |-> ( C R D ) ) = ( z e. ( A X. B ) |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ ( C R D ) )
69 67 68 eqtr4i 
 |-  ( z e. ( A X. B ) |-> ( [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ C R [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ D ) ) = ( x e. A , y e. B |-> ( C R D ) )
70 60 69 eqtrdi 
 |-  ( ph -> ( F oF R G ) = ( x e. A , y e. B |-> ( C R D ) ) )