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 φ A V
offval22.b φ B W
offval22.c φ x A y B C X
offval22.d φ x A y B D Y
offval22.f φ F = x A , y B C
offval22.g φ G = x A , y B D
Assertion offval22 φ F R f G = x A , y B C R D

Proof

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