Step | Hyp | Ref
| Expression |
1 | | offval22.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | offval22.b |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
3 | | xpexg 6858 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 × 𝐵) ∈ V) |
4 | 1, 2, 3 | syl2anc 691 |
. . 3
⊢ (𝜑 → (𝐴 × 𝐵) ∈ V) |
5 | | xp1st 7089 |
. . . . 5
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (1st ‘𝑧) ∈ 𝐴) |
6 | | xp2nd 7090 |
. . . . 5
⊢ (𝑧 ∈ (𝐴 × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
7 | 5, 6 | jca 553 |
. . . 4
⊢ (𝑧 ∈ (𝐴 × 𝐵) → ((1st ‘𝑧) ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵)) |
8 | | fvex 6113 |
. . . . . 6
⊢
(2nd ‘𝑧) ∈ V |
9 | | fvex 6113 |
. . . . . 6
⊢
(1st ‘𝑧) ∈ V |
10 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑦(2nd ‘𝑧) |
11 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥(2nd ‘𝑧) |
12 | | nfcv 2751 |
. . . . . . 7
⊢
Ⅎ𝑥(1st ‘𝑧) |
13 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) |
14 | | nfcsb1v 3515 |
. . . . . . . . 9
⊢
Ⅎ𝑦⦋(2nd ‘𝑧) / 𝑦⦌𝐶 |
15 | 14 | nfel1 2765 |
. . . . . . . 8
⊢
Ⅎ𝑦⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V |
16 | 13, 15 | nfim 1813 |
. . . . . . 7
⊢
Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
17 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) |
18 | | nfcsb1v 3515 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 |
19 | 18 | nfel1 2765 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V |
20 | 17, 19 | nfim 1813 |
. . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
21 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘𝑧) → (𝑦 ∈ 𝐵 ↔ (2nd ‘𝑧) ∈ 𝐵)) |
22 | 21 | 3anbi3d 1397 |
. . . . . . . 8
⊢ (𝑦 = (2nd ‘𝑧) → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵))) |
23 | | csbeq1a 3508 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘𝑧) → 𝐶 = ⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
24 | 23 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑦 = (2nd ‘𝑧) → (𝐶 ∈ V ↔
⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V)) |
25 | 22, 24 | imbi12d 333 |
. . . . . . 7
⊢ (𝑦 = (2nd ‘𝑧) → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ V) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V))) |
26 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑧) → (𝑥 ∈ 𝐴 ↔ (1st ‘𝑧) ∈ 𝐴)) |
27 | 26 | 3anbi2d 1396 |
. . . . . . . 8
⊢ (𝑥 = (1st ‘𝑧) → ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) ↔ (𝜑 ∧ (1st ‘𝑧) ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵))) |
28 | | csbeq1a 3508 |
. . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑧) →
⦋(2nd ‘𝑧) / 𝑦⦌𝐶 = ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
29 | 28 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = (1st ‘𝑧) →
(⦋(2nd ‘𝑧) / 𝑦⦌𝐶 ∈ V ↔
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V)) |
30 | 27, 29 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = (1st ‘𝑧) → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) ↔ ((𝜑 ∧ (1st ‘𝑧) ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V))) |
31 | | offval22.c |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ 𝑋) |
32 | | elex 3185 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑋 → 𝐶 ∈ V) |
33 | 31, 32 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ V) |
34 | 10, 11, 12, 16, 20, 25, 30, 33 | vtocl2gf 3241 |
. . . . . 6
⊢
(((2nd ‘𝑧) ∈ V ∧ (1st ‘𝑧) ∈ V) → ((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V)) |
35 | 8, 9, 34 | mp2an 704 |
. . . . 5
⊢ ((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
36 | 35 | 3expb 1258 |
. . . 4
⊢ ((𝜑 ∧ ((1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵)) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
37 | 7, 36 | sylan2 490 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 × 𝐵)) → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶 ∈ V) |
38 | | nfcsb1v 3515 |
. . . . . . . . 9
⊢
Ⅎ𝑦⦋(2nd ‘𝑧) / 𝑦⦌𝐷 |
39 | 38 | nfel1 2765 |
. . . . . . . 8
⊢
Ⅎ𝑦⦋(2nd ‘𝑧) / 𝑦⦌𝐷 ∈ V |
40 | 13, 39 | nfim 1813 |
. . . . . . 7
⊢
Ⅎ𝑦((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) |
41 | | nfcsb1v 3515 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 |
42 | 41 | nfel1 2765 |
. . . . . . . 8
⊢
Ⅎ𝑥⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V |
43 | 17, 42 | nfim 1813 |
. . . . . . 7
⊢
Ⅎ𝑥((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) |
44 | | csbeq1a 3508 |
. . . . . . . . 9
⊢ (𝑦 = (2nd ‘𝑧) → 𝐷 = ⦋(2nd
‘𝑧) / 𝑦⦌𝐷) |
45 | 44 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑦 = (2nd ‘𝑧) → (𝐷 ∈ V ↔
⦋(2nd ‘𝑧) / 𝑦⦌𝐷 ∈ V)) |
46 | 22, 45 | imbi12d 333 |
. . . . . . 7
⊢ (𝑦 = (2nd ‘𝑧) → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ V) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V))) |
47 | | csbeq1a 3508 |
. . . . . . . . 9
⊢ (𝑥 = (1st ‘𝑧) →
⦋(2nd ‘𝑧) / 𝑦⦌𝐷 = ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷) |
48 | 47 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑥 = (1st ‘𝑧) →
(⦋(2nd ‘𝑧) / 𝑦⦌𝐷 ∈ V ↔
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V)) |
49 | 27, 48 | imbi12d 333 |
. . . . . . 7
⊢ (𝑥 = (1st ‘𝑧) → (((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) ↔ ((𝜑 ∧ (1st ‘𝑧) ∈ 𝐴 ∧ (2nd ‘𝑧) ∈ 𝐵) → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V))) |
50 | | offval22.d |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ 𝑌) |
51 | | elex 3185 |
. . . . . . . 8
⊢ (𝐷 ∈ 𝑌 → 𝐷 ∈ V) |
52 | 50, 51 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ V) |
53 | 10, 11, 12, 40, 43, 46, 49, 52 | vtocl2gf 3241 |
. . . . . 6
⊢
(((2nd ‘𝑧) ∈ V ∧ (1st ‘𝑧) ∈ V) → ((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V)) |
54 | 8, 9, 53 | mp2an 704 |
. . . . 5
⊢ ((𝜑 ∧ (1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) |
55 | 54 | 3expb 1258 |
. . . 4
⊢ ((𝜑 ∧ ((1st
‘𝑧) ∈ 𝐴 ∧ (2nd
‘𝑧) ∈ 𝐵)) →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) |
56 | 7, 55 | sylan2 490 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 × 𝐵)) → ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷 ∈ V) |
57 | | offval22.f |
. . . 4
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶)) |
58 | | mpt2mpts 7123 |
. . . 4
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶) |
59 | 57, 58 | syl6eq 2660 |
. . 3
⊢ (𝜑 → 𝐹 = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶)) |
60 | | offval22.g |
. . . 4
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
61 | | mpt2mpts 7123 |
. . . 4
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷) |
62 | 60, 61 | syl6eq 2660 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷)) |
63 | 4, 37, 56, 59, 62 | offval2 6812 |
. 2
⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑧 ∈ (𝐴 × 𝐵) ↦ (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷))) |
64 | | csbov12g 6587 |
. . . . . . 7
⊢
((2nd ‘𝑧) ∈ V →
⦋(2nd ‘𝑧) / 𝑦⦌(𝐶𝑅𝐷) = (⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(2nd ‘𝑧) / 𝑦⦌𝐷)) |
65 | 64 | csbeq2dv 3944 |
. . . . . 6
⊢
((2nd ‘𝑧) ∈ V →
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌(𝐶𝑅𝐷) = ⦋(1st
‘𝑧) / 𝑥⦌(⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(2nd ‘𝑧) / 𝑦⦌𝐷)) |
66 | 8, 65 | ax-mp 5 |
. . . . 5
⊢
⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌(𝐶𝑅𝐷) = ⦋(1st
‘𝑧) / 𝑥⦌(⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(2nd ‘𝑧) / 𝑦⦌𝐷) |
67 | | csbov12g 6587 |
. . . . . 6
⊢
((1st ‘𝑧) ∈ V →
⦋(1st ‘𝑧) / 𝑥⦌(⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(2nd ‘𝑧) / 𝑦⦌𝐷) = (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷)) |
68 | 9, 67 | ax-mp 5 |
. . . . 5
⊢
⦋(1st ‘𝑧) / 𝑥⦌(⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(2nd ‘𝑧) / 𝑦⦌𝐷) = (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷) |
69 | 66, 68 | eqtr2i 2633 |
. . . 4
⊢
(⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷) = ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌(𝐶𝑅𝐷) |
70 | 69 | mpteq2i 4669 |
. . 3
⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷)) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌(𝐶𝑅𝐷)) |
71 | | mpt2mpts 7123 |
. . 3
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑅𝐷)) = (𝑧 ∈ (𝐴 × 𝐵) ↦ ⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌(𝐶𝑅𝐷)) |
72 | 70, 71 | eqtr4i 2635 |
. 2
⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ (⦋(1st
‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐶𝑅⦋(1st ‘𝑧) / 𝑥⦌⦋(2nd
‘𝑧) / 𝑦⦌𝐷)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑅𝐷)) |
73 | 63, 72 | syl6eq 2660 |
1
⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ (𝐶𝑅𝐷))) |