# 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 ( 𝜑𝐴𝑉 )
offval22.b ( 𝜑𝐵𝑊 )
offval22.c ( ( 𝜑𝑥𝐴𝑦𝐵 ) → 𝐶𝑋 )
offval22.d ( ( 𝜑𝑥𝐴𝑦𝐵 ) → 𝐷𝑌 )
offval22.f ( 𝜑𝐹 = ( 𝑥𝐴 , 𝑦𝐵𝐶 ) )
offval22.g ( 𝜑𝐺 = ( 𝑥𝐴 , 𝑦𝐵𝐷 ) )
Assertion offval22 ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) = ( 𝑥𝐴 , 𝑦𝐵 ↦ ( 𝐶 𝑅 𝐷 ) ) )

### Proof

Step Hyp Ref Expression
1 offval22.a ( 𝜑𝐴𝑉 )
2 offval22.b ( 𝜑𝐵𝑊 )
3 offval22.c ( ( 𝜑𝑥𝐴𝑦𝐵 ) → 𝐶𝑋 )
4 offval22.d ( ( 𝜑𝑥𝐴𝑦𝐵 ) → 𝐷𝑌 )
5 offval22.f ( 𝜑𝐹 = ( 𝑥𝐴 , 𝑦𝐵𝐶 ) )
6 offval22.g ( 𝜑𝐺 = ( 𝑥𝐴 , 𝑦𝐵𝐷 ) )
7 1 2 xpexd ( 𝜑 → ( 𝐴 × 𝐵 ) ∈ V )
8 xp1st ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( 1st𝑧 ) ∈ 𝐴 )
9 xp2nd ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( 2nd𝑧 ) ∈ 𝐵 )
10 8 9 jca ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) )
11 fvex ( 2nd𝑧 ) ∈ V
12 fvex ( 1st𝑧 ) ∈ V
13 nfcv 𝑦 ( 2nd𝑧 )
14 nfcv 𝑥 ( 2nd𝑧 )
15 nfcv 𝑥 ( 1st𝑧 )
16 nfv 𝑦 ( 𝜑𝑥𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 )
17 nfcsb1v 𝑦 ( 2nd𝑧 ) / 𝑦 𝐶
18 17 nfel1 𝑦 ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V
19 16 18 nfim 𝑦 ( ( 𝜑𝑥𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V )
20 nfv 𝑥 ( 𝜑 ∧ ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 )
21 nfcsb1v 𝑥 ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶
22 21 nfel1 𝑥 ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V
23 20 22 nfim 𝑥 ( ( 𝜑 ∧ ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V )
24 eleq1 ( 𝑦 = ( 2nd𝑧 ) → ( 𝑦𝐵 ↔ ( 2nd𝑧 ) ∈ 𝐵 ) )
25 24 3anbi3d ( 𝑦 = ( 2nd𝑧 ) → ( ( 𝜑𝑥𝐴𝑦𝐵 ) ↔ ( 𝜑𝑥𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) ) )
26 csbeq1a ( 𝑦 = ( 2nd𝑧 ) → 𝐶 = ( 2nd𝑧 ) / 𝑦 𝐶 )
27 26 eleq1d ( 𝑦 = ( 2nd𝑧 ) → ( 𝐶 ∈ V ↔ ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V ) )
28 25 27 imbi12d ( 𝑦 = ( 2nd𝑧 ) → ( ( ( 𝜑𝑥𝐴𝑦𝐵 ) → 𝐶 ∈ V ) ↔ ( ( 𝜑𝑥𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V ) ) )
29 eleq1 ( 𝑥 = ( 1st𝑧 ) → ( 𝑥𝐴 ↔ ( 1st𝑧 ) ∈ 𝐴 ) )
30 29 3anbi2d ( 𝑥 = ( 1st𝑧 ) → ( ( 𝜑𝑥𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) ↔ ( 𝜑 ∧ ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) ) )
31 csbeq1a ( 𝑥 = ( 1st𝑧 ) → ( 2nd𝑧 ) / 𝑦 𝐶 = ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 )
32 31 eleq1d ( 𝑥 = ( 1st𝑧 ) → ( ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V ↔ ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V ) )
33 30 32 imbi12d ( 𝑥 = ( 1st𝑧 ) → ( ( ( 𝜑𝑥𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V ) ↔ ( ( 𝜑 ∧ ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V ) ) )
34 3 elexd ( ( 𝜑𝑥𝐴𝑦𝐵 ) → 𝐶 ∈ V )
35 13 14 15 19 23 28 33 34 vtocl2gf ( ( ( 2nd𝑧 ) ∈ V ∧ ( 1st𝑧 ) ∈ V ) → ( ( 𝜑 ∧ ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V ) )
36 11 12 35 mp2an ( ( 𝜑 ∧ ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V )
37 36 3expb ( ( 𝜑 ∧ ( ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V )
38 10 37 sylan2 ( ( 𝜑𝑧 ∈ ( 𝐴 × 𝐵 ) ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 ∈ V )
39 nfcsb1v 𝑦 ( 2nd𝑧 ) / 𝑦 𝐷
40 39 nfel1 𝑦 ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V
41 16 40 nfim 𝑦 ( ( 𝜑𝑥𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V )
42 nfcsb1v 𝑥 ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷
43 42 nfel1 𝑥 ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V
44 20 43 nfim 𝑥 ( ( 𝜑 ∧ ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V )
45 csbeq1a ( 𝑦 = ( 2nd𝑧 ) → 𝐷 = ( 2nd𝑧 ) / 𝑦 𝐷 )
46 45 eleq1d ( 𝑦 = ( 2nd𝑧 ) → ( 𝐷 ∈ V ↔ ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V ) )
47 25 46 imbi12d ( 𝑦 = ( 2nd𝑧 ) → ( ( ( 𝜑𝑥𝐴𝑦𝐵 ) → 𝐷 ∈ V ) ↔ ( ( 𝜑𝑥𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V ) ) )
48 csbeq1a ( 𝑥 = ( 1st𝑧 ) → ( 2nd𝑧 ) / 𝑦 𝐷 = ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 )
49 48 eleq1d ( 𝑥 = ( 1st𝑧 ) → ( ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V ↔ ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V ) )
50 30 49 imbi12d ( 𝑥 = ( 1st𝑧 ) → ( ( ( 𝜑𝑥𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V ) ↔ ( ( 𝜑 ∧ ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V ) ) )
51 4 elexd ( ( 𝜑𝑥𝐴𝑦𝐵 ) → 𝐷 ∈ V )
52 13 14 15 41 44 47 50 51 vtocl2gf ( ( ( 2nd𝑧 ) ∈ V ∧ ( 1st𝑧 ) ∈ V ) → ( ( 𝜑 ∧ ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V ) )
53 11 12 52 mp2an ( ( 𝜑 ∧ ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V )
54 53 3expb ( ( 𝜑 ∧ ( ( 1st𝑧 ) ∈ 𝐴 ∧ ( 2nd𝑧 ) ∈ 𝐵 ) ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V )
55 10 54 sylan2 ( ( 𝜑𝑧 ∈ ( 𝐴 × 𝐵 ) ) → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ∈ V )
56 mpompts ( 𝑥𝐴 , 𝑦𝐵𝐶 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 )
57 5 56 eqtrdi ( 𝜑𝐹 = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 ) )
58 mpompts ( 𝑥𝐴 , 𝑦𝐵𝐷 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 )
59 6 58 eqtrdi ( 𝜑𝐺 = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ) )
60 7 38 55 57 59 offval2 ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 𝑅 ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ) ) )
61 csbov12g ( ( 2nd𝑧 ) ∈ V → ( 2nd𝑧 ) / 𝑦 ( 𝐶 𝑅 𝐷 ) = ( ( 2nd𝑧 ) / 𝑦 𝐶 𝑅 ( 2nd𝑧 ) / 𝑦 𝐷 ) )
62 61 csbeq2dv ( ( 2nd𝑧 ) ∈ V → ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 ( 𝐶 𝑅 𝐷 ) = ( 1st𝑧 ) / 𝑥 ( ( 2nd𝑧 ) / 𝑦 𝐶 𝑅 ( 2nd𝑧 ) / 𝑦 𝐷 ) )
63 11 62 ax-mp ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 ( 𝐶 𝑅 𝐷 ) = ( 1st𝑧 ) / 𝑥 ( ( 2nd𝑧 ) / 𝑦 𝐶 𝑅 ( 2nd𝑧 ) / 𝑦 𝐷 )
64 csbov12g ( ( 1st𝑧 ) ∈ V → ( 1st𝑧 ) / 𝑥 ( ( 2nd𝑧 ) / 𝑦 𝐶 𝑅 ( 2nd𝑧 ) / 𝑦 𝐷 ) = ( ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 𝑅 ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ) )
65 12 64 ax-mp ( 1st𝑧 ) / 𝑥 ( ( 2nd𝑧 ) / 𝑦 𝐶 𝑅 ( 2nd𝑧 ) / 𝑦 𝐷 ) = ( ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 𝑅 ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 )
66 63 65 eqtr2i ( ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 𝑅 ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ) = ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 ( 𝐶 𝑅 𝐷 )
67 66 mpteq2i ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 𝑅 ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ) ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 ( 𝐶 𝑅 𝐷 ) )
68 mpompts ( 𝑥𝐴 , 𝑦𝐵 ↦ ( 𝐶 𝑅 𝐷 ) ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 ( 𝐶 𝑅 𝐷 ) )
69 67 68 eqtr4i ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐶 𝑅 ( 1st𝑧 ) / 𝑥 ( 2nd𝑧 ) / 𝑦 𝐷 ) ) = ( 𝑥𝐴 , 𝑦𝐵 ↦ ( 𝐶 𝑅 𝐷 ) )
70 60 69 eqtrdi ( 𝜑 → ( 𝐹f 𝑅 𝐺 ) = ( 𝑥𝐴 , 𝑦𝐵 ↦ ( 𝐶 𝑅 𝐷 ) ) )