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 
⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ) 
9 

xp2nd 
⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) 
10 
8 9

jca 
⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) → ( ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) ) 
11 

fvex 
⊢ ( 2^{nd} ‘ 𝑧 ) ∈ V 
12 

fvex 
⊢ ( 1^{st} ‘ 𝑧 ) ∈ V 
13 

nfcv 
⊢ Ⅎ 𝑦 ( 2^{nd} ‘ 𝑧 ) 
14 

nfcv 
⊢ Ⅎ 𝑥 ( 2^{nd} ‘ 𝑧 ) 
15 

nfcv 
⊢ Ⅎ 𝑥 ( 1^{st} ‘ 𝑧 ) 
16 

nfv 
⊢ Ⅎ 𝑦 ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) 
17 

nfcsb1v 
⊢ Ⅎ 𝑦 ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 
18 
17

nfel1 
⊢ Ⅎ 𝑦 ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V 
19 
16 18

nfim 
⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) 
20 

nfv 
⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) 
21 

nfcsb1v 
⊢ Ⅎ 𝑥 ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 
22 
21

nfel1 
⊢ Ⅎ 𝑥 ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V 
23 
20 22

nfim 
⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) 
24 

eleq1 
⊢ ( 𝑦 = ( 2^{nd} ‘ 𝑧 ) → ( 𝑦 ∈ 𝐵 ↔ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) ) 
25 
24

3anbi3d 
⊢ ( 𝑦 = ( 2^{nd} ‘ 𝑧 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) ) ) 
26 

csbeq1a 
⊢ ( 𝑦 = ( 2^{nd} ‘ 𝑧 ) → 𝐶 = ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ) 
27 
26

eleq1d 
⊢ ( 𝑦 = ( 2^{nd} ‘ 𝑧 ) → ( 𝐶 ∈ V ↔ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) ) 
28 
25 27

imbi12d 
⊢ ( 𝑦 = ( 2^{nd} ‘ 𝑧 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ V ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) ) ) 
29 

eleq1 
⊢ ( 𝑥 = ( 1^{st} ‘ 𝑧 ) → ( 𝑥 ∈ 𝐴 ↔ ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ) ) 
30 
29

3anbi2d 
⊢ ( 𝑥 = ( 1^{st} ‘ 𝑧 ) → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) ↔ ( 𝜑 ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) ) ) 
31 

csbeq1a 
⊢ ( 𝑥 = ( 1^{st} ‘ 𝑧 ) → ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 = ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ) 
32 
31

eleq1d 
⊢ ( 𝑥 = ( 1^{st} ‘ 𝑧 ) → ( ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ↔ ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) ) 
33 
30 32

imbi12d 
⊢ ( 𝑥 = ( 1^{st} ‘ 𝑧 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) ↔ ( ( 𝜑 ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) ) ) 
34 
3

elexd 
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ V ) 
35 
13 14 15 19 23 28 33 34

vtocl2gf 
⊢ ( ( ( 2^{nd} ‘ 𝑧 ) ∈ V ∧ ( 1^{st} ‘ 𝑧 ) ∈ V ) → ( ( 𝜑 ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) ) 
36 
11 12 35

mp2an 
⊢ ( ( 𝜑 ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) 
37 
36

3expb 
⊢ ( ( 𝜑 ∧ ( ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) 
38 
10 37

sylan2 
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 × 𝐵 ) ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ∈ V ) 
39 

nfcsb1v 
⊢ Ⅎ 𝑦 ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 
40 
39

nfel1 
⊢ Ⅎ 𝑦 ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V 
41 
16 40

nfim 
⊢ Ⅎ 𝑦 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) 
42 

nfcsb1v 
⊢ Ⅎ 𝑥 ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 
43 
42

nfel1 
⊢ Ⅎ 𝑥 ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V 
44 
20 43

nfim 
⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) 
45 

csbeq1a 
⊢ ( 𝑦 = ( 2^{nd} ‘ 𝑧 ) → 𝐷 = ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) 
46 
45

eleq1d 
⊢ ( 𝑦 = ( 2^{nd} ‘ 𝑧 ) → ( 𝐷 ∈ V ↔ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) ) 
47 
25 46

imbi12d 
⊢ ( 𝑦 = ( 2^{nd} ‘ 𝑧 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ V ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) ) ) 
48 

csbeq1a 
⊢ ( 𝑥 = ( 1^{st} ‘ 𝑧 ) → ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 = ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) 
49 
48

eleq1d 
⊢ ( 𝑥 = ( 1^{st} ‘ 𝑧 ) → ( ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ↔ ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) ) 
50 
30 49

imbi12d 
⊢ ( 𝑥 = ( 1^{st} ‘ 𝑧 ) → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) ↔ ( ( 𝜑 ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) ) ) 
51 
4

elexd 
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → 𝐷 ∈ V ) 
52 
13 14 15 41 44 47 50 51

vtocl2gf 
⊢ ( ( ( 2^{nd} ‘ 𝑧 ) ∈ V ∧ ( 1^{st} ‘ 𝑧 ) ∈ V ) → ( ( 𝜑 ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) ) 
53 
11 12 52

mp2an 
⊢ ( ( 𝜑 ∧ ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) 
54 
53

3expb 
⊢ ( ( 𝜑 ∧ ( ( 1^{st} ‘ 𝑧 ) ∈ 𝐴 ∧ ( 2^{nd} ‘ 𝑧 ) ∈ 𝐵 ) ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) 
55 
10 54

sylan2 
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 × 𝐵 ) ) → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ∈ V ) 
56 

mpompts 
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ) 
57 
5 56

eqtrdi 
⊢ ( 𝜑 → 𝐹 = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 ) ) 
58 

mpompts 
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐷 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) 
59 
6 58

eqtrdi 
⊢ ( 𝜑 → 𝐺 = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) ) 
60 
7 38 55 57 59

offval2 
⊢ ( 𝜑 → ( 𝐹 ∘_{f} 𝑅 𝐺 ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) ) ) 
61 

csbov12g 
⊢ ( ( 2^{nd} ‘ 𝑧 ) ∈ V → ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 ) = ( ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) ) 
62 
61

csbeq2dv 
⊢ ( ( 2^{nd} ‘ 𝑧 ) ∈ V → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 ) = ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ( ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) ) 
63 
11 62

axmp 
⊢ ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 ) = ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ( ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) 
64 

csbov12g 
⊢ ( ( 1^{st} ‘ 𝑧 ) ∈ V → ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ( ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) = ( ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) ) 
65 
12 64

axmp 
⊢ ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ( ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) = ( ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) 
66 
63 65

eqtr2i 
⊢ ( ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) = ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 ) 
67 
66

mpteq2i 
⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 ) ) 
68 

mpompts 
⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑅 𝐷 ) ) = ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ ( 𝐶 𝑅 𝐷 ) ) 
69 
67 68

eqtr4i 
⊢ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ ( ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐶 𝑅 ⦋ ( 1^{st} ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2^{nd} ‘ 𝑧 ) / 𝑦 ⦌ 𝐷 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑅 𝐷 ) ) 
70 
60 69

eqtrdi 
⊢ ( 𝜑 → ( 𝐹 ∘_{f} 𝑅 𝐺 ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ ( 𝐶 𝑅 𝐷 ) ) ) 