Step | Hyp | Ref
| Expression |
1 | | offval22.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | offval22.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
3 | 1, 2 | xpexd 7601 |
. . 3
⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
4 | | xp1st 7863 |
. . . . 5
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (1st ‘𝑧) ∈ 𝐴) |
5 | | xp2nd 7864 |
. . . . 5
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
6 | 4, 5 | jca 512 |
. . . 4
⊢ (𝑧 ∈ (𝐴 × 𝐵) → ((1st ‘𝑧) ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵)) |
7 | | fvex 6787 |
. . . . . 6
⊢
(2nd ‘𝑧) ∈ V |
8 | | fvex 6787 |
. . . . . 6
⊢
(1st ‘𝑧) ∈ V |
9 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑦(2nd ‘𝑧) |
10 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑥(2nd ‘𝑧) |
11 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑥(1st ‘𝑧) |
12 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) |
13 | | nfcsb1v 3857 |
. . . . . . . . 9
⊢
Ⅎ𝑦⦋(2nd ‘𝑧) / 𝑦⦌𝐶 |
14 | 13 | nfel1 2923 |
. . . . . . . 8
⊢
Ⅎ𝑦⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V |
15 | 12, 14 | nfim 1899 |
. . . . . . 7
⊢
Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
16 | | nfv 1917 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) |
17 | | nfcsb1v 3857 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 |
18 | 17 | nfel1 2923 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V |
19 | 16, 18 | nfim 1899 |
. . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
20 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘𝑧) → (𝑦 ∈ 𝐵 ↔ (2nd ‘𝑧) ∈ 𝐵)) |
21 | 20 | 3anbi3d 1441 |
. . . . . . . 8
⊢ (𝑦 = (2nd ‘𝑧) → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵))) |
22 | | csbeq1a 3846 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘𝑧) → 𝐶 = ⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
23 | 22 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑦 = (2nd ‘𝑧) → (𝐶 ∈ V ↔
⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V)) |
24 | 21, 23 | imbi12d 345 |
. . . . . . 7
⊢ (𝑦 = (2nd ‘𝑧) → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ V) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V))) |
25 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑧) → (𝑥 ∈ 𝐴 ↔ (1st ‘𝑧) ∈ 𝐴)) |
26 | 25 | 3anbi2d 1440 |
. . . . . . . 8
⊢ (𝑥 = (1st ‘𝑧) → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) ↔ (𝜑 ∧ (1st ‘𝑧) ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵))) |
27 | | csbeq1a 3846 |
. . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑧) →
⦋(2nd ‘𝑧) / 𝑦⦌𝐶 = ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
28 | 27 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑥 = (1st ‘𝑧) →
(⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V ↔
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V)) |
29 | 26, 28 | imbi12d 345 |
. . . . . . 7
⊢ (𝑥 = (1st ‘𝑧) → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) ↔ ((𝜑 ∧ (1st ‘𝑧) ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V))) |
30 | | offval22.c |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝑋) |
31 | 30 | elexd 3452 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ V) |
32 | 9, 10, 11, 15, 19, 24, 29, 31 | vtocl2gf 3508 |
. . . . . 6
⊢
(((2nd ‘𝑧) ∈ V ∧ (1st ‘𝑧) ∈ V) → ((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V)) |
33 | 7, 8, 32 | mp2an 689 |
. . . . 5
⊢ ((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
34 | 33 | 3expb 1119 |
. . . 4
⊢ ((𝜑 ∧ ((1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵)) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
35 | 6, 34 | sylan2 593 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 × 𝐵)) → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
36 | | nfcsb1v 3857 |
. . . . . . . . 9
⊢
Ⅎ𝑦⦋(2nd ‘𝑧) / 𝑦⦌𝐷 |
37 | 36 | nfel1 2923 |
. . . . . . . 8
⊢
Ⅎ𝑦⦋(2nd ‘𝑧) / 𝑦⦌𝐷 ∈ V |
38 | 12, 37 | nfim 1899 |
. . . . . . 7
⊢
Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) |
39 | | nfcsb1v 3857 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 |
40 | 39 | nfel1 2923 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V |
41 | 16, 40 | nfim 1899 |
. . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) |
42 | | csbeq1a 3846 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘𝑧) → 𝐷 = ⦋(2nd
‘𝑧) / 𝑦⦌𝐷) |
43 | 42 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑦 = (2nd ‘𝑧) → (𝐷 ∈ V ↔
⦋(2nd ‘𝑧) / 𝑦⦌𝐷 ∈ V)) |
44 | 21, 43 | imbi12d 345 |
. . . . . . 7
⊢ (𝑦 = (2nd ‘𝑧) → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ V) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V))) |
45 | | csbeq1a 3846 |
. . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑧) →
⦋(2nd ‘𝑧) / 𝑦⦌𝐷 = ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷) |
46 | 45 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑥 = (1st ‘𝑧) →
(⦋(2nd ‘𝑧) / 𝑦⦌𝐷 ∈ V ↔
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V)) |
47 | 26, 46 | imbi12d 345 |
. . . . . . 7
⊢ (𝑥 = (1st ‘𝑧) → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) ↔ ((𝜑 ∧ (1st ‘𝑧) ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V))) |
48 | | offval22.d |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑌) |
49 | 48 | elexd 3452 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ V) |
50 | 9, 10, 11, 38, 41, 44, 47, 49 | vtocl2gf 3508 |
. . . . . 6
⊢
(((2nd ‘𝑧) ∈ V ∧ (1st ‘𝑧) ∈ V) → ((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V)) |
51 | 7, 8, 50 | mp2an 689 |
. . . . 5
⊢ ((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) |
52 | 51 | 3expb 1119 |
. . . 4
⊢ ((𝜑 ∧ ((1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵)) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) |
53 | 6, 52 | sylan2 593 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 × 𝐵)) → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) |
54 | | offval22.f |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)) |
55 | | mpompts 7905 |
. . . 4
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
56 | 54, 55 | eqtrdi 2794 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶)) |
57 | | offval22.g |
. . . 4
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
58 | | mpompts 7905 |
. . . 4
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷) |
59 | 57, 58 | eqtrdi 2794 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷)) |
60 | 3, 35, 53, 56, 59 | offval2 7553 |
. 2
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑧 ∈ (𝐴 × 𝐵) ↦ (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷))) |
61 | | csbov12g 7319 |
. . . . . . 7
⊢
((2nd ‘𝑧) ∈ V →
⦋(2nd ‘𝑧) / 𝑦⦌(𝐶𝑅𝐷) = (⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(2nd ‘𝑧) / 𝑦⦌𝐷)) |
62 | 61 | csbeq2dv 3839 |
. . . . . 6
⊢
((2nd ‘𝑧) ∈ V →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌(𝐶𝑅𝐷) = ⦋(1st
‘𝑧) / 𝑥⦌(⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(2nd ‘𝑧) / 𝑦⦌𝐷)) |
63 | 7, 62 | ax-mp 5 |
. . . . 5
⊢
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌(𝐶𝑅𝐷) = ⦋(1st
‘𝑧) / 𝑥⦌(⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(2nd ‘𝑧) / 𝑦⦌𝐷) |
64 | | csbov12g 7319 |
. . . . . 6
⊢
((1st ‘𝑧) ∈ V →
⦋(1st ‘𝑧) / 𝑥⦌(⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(2nd ‘𝑧) / 𝑦⦌𝐷) = (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷)) |
65 | 8, 64 | ax-mp 5 |
. . . . 5
⊢
⦋(1st ‘𝑧) / 𝑥⦌(⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(2nd ‘𝑧) / 𝑦⦌𝐷) = (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷) |
66 | 63, 65 | eqtr2i 2767 |
. . . 4
⊢
(⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷) = ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌(𝐶𝑅𝐷) |
67 | 66 | mpteq2i 5179 |
. . 3
⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷)) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌(𝐶𝑅𝐷)) |
68 | | mpompts 7905 |
. . 3
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑅𝐷)) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌(𝐶𝑅𝐷)) |
69 | 67, 68 | eqtr4i 2769 |
. 2
⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑅𝐷)) |
70 | 60, 69 | eqtrdi 2794 |
1
⊢ (𝜑 → (𝐹 ∘f 𝑅𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑅𝐷))) |