# 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 ) ) )`