Step | Hyp | Ref
| Expression |
1 | | offval.1 |
. . . 4
⊢ (φ → 𝐹 Fn A) |
2 | | offval.3 |
. . . 4
⊢ (φ → A ∈ 𝑉) |
3 | | fnex 5326 |
. . . 4
⊢ ((𝐹 Fn A ∧ A ∈ 𝑉) → 𝐹 ∈
V) |
4 | 1, 2, 3 | syl2anc 391 |
. . 3
⊢ (φ → 𝐹 ∈
V) |
5 | | offval.2 |
. . . 4
⊢ (φ → 𝐺 Fn B) |
6 | | offval.4 |
. . . 4
⊢ (φ → B ∈ 𝑊) |
7 | | fnex 5326 |
. . . 4
⊢ ((𝐺 Fn B ∧ B ∈ 𝑊) → 𝐺 ∈
V) |
8 | 5, 6, 7 | syl2anc 391 |
. . 3
⊢ (φ → 𝐺 ∈
V) |
9 | | dmeq 4478 |
. . . . . 6
⊢ (f = 𝐹 → dom f = dom 𝐹) |
10 | | dmeq 4478 |
. . . . . 6
⊢ (g = 𝐺 → dom g = dom 𝐺) |
11 | 9, 10 | ineqan12d 3134 |
. . . . 5
⊢
((f = 𝐹 ∧ g = 𝐺) → (dom f ∩ dom g) =
(dom 𝐹 ∩ dom 𝐺)) |
12 | | fveq1 5120 |
. . . . . 6
⊢ (f = 𝐹 → (f‘x) =
(𝐹‘x)) |
13 | | fveq1 5120 |
. . . . . 6
⊢ (g = 𝐺 → (g‘x) =
(𝐺‘x)) |
14 | 12, 13 | breqan12d 3770 |
. . . . 5
⊢
((f = 𝐹 ∧ g = 𝐺) → ((f‘x)𝑅(g‘x)
↔ (𝐹‘x)𝑅(𝐺‘x))) |
15 | 11, 14 | raleqbidv 2511 |
. . . 4
⊢
((f = 𝐹 ∧ g = 𝐺) → (∀x ∈ (dom f ∩
dom g)(f‘x)𝑅(g‘x)
↔ ∀x ∈ (dom 𝐹 ∩ dom 𝐺)(𝐹‘x)𝑅(𝐺‘x))) |
16 | | df-ofr 5655 |
. . . 4
⊢
∘𝑟 𝑅 = {〈f, g〉
∣ ∀x ∈ (dom f ∩ dom g)(f‘x)𝑅(g‘x)} |
17 | 15, 16 | brabga 3992 |
. . 3
⊢ ((𝐹 ∈ V ∧ 𝐺 ∈ V) → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀x ∈ (dom 𝐹 ∩ dom 𝐺)(𝐹‘x)𝑅(𝐺‘x))) |
18 | 4, 8, 17 | syl2anc 391 |
. 2
⊢ (φ → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀x ∈ (dom 𝐹 ∩ dom 𝐺)(𝐹‘x)𝑅(𝐺‘x))) |
19 | | fndm 4941 |
. . . . . 6
⊢ (𝐹 Fn A → dom 𝐹 = A) |
20 | 1, 19 | syl 14 |
. . . . 5
⊢ (φ → dom 𝐹 = A) |
21 | | fndm 4941 |
. . . . . 6
⊢ (𝐺 Fn B → dom 𝐺 = B) |
22 | 5, 21 | syl 14 |
. . . . 5
⊢ (φ → dom 𝐺 = B) |
23 | 20, 22 | ineq12d 3133 |
. . . 4
⊢ (φ → (dom 𝐹 ∩ dom 𝐺) = (A
∩ B)) |
24 | | offval.5 |
. . . 4
⊢ (A ∩ B) =
𝑆 |
25 | 23, 24 | syl6eq 2085 |
. . 3
⊢ (φ → (dom 𝐹 ∩ dom 𝐺) = 𝑆) |
26 | 25 | raleqdv 2505 |
. 2
⊢ (φ → (∀x ∈ (dom 𝐹 ∩ dom 𝐺)(𝐹‘x)𝑅(𝐺‘x) ↔ ∀x ∈ 𝑆 (𝐹‘x)𝑅(𝐺‘x))) |
27 | | inss1 3151 |
. . . . . . 7
⊢ (A ∩ B)
⊆ A |
28 | 24, 27 | eqsstr3i 2970 |
. . . . . 6
⊢ 𝑆 ⊆ A |
29 | 28 | sseli 2935 |
. . . . 5
⊢ (x ∈ 𝑆 → x ∈ A) |
30 | | offval.6 |
. . . . 5
⊢ ((φ ∧ x ∈ A) → (𝐹‘x) = 𝐶) |
31 | 29, 30 | sylan2 270 |
. . . 4
⊢ ((φ ∧ x ∈ 𝑆) → (𝐹‘x) = 𝐶) |
32 | | inss2 3152 |
. . . . . . 7
⊢ (A ∩ B)
⊆ B |
33 | 24, 32 | eqsstr3i 2970 |
. . . . . 6
⊢ 𝑆 ⊆ B |
34 | 33 | sseli 2935 |
. . . . 5
⊢ (x ∈ 𝑆 → x ∈ B) |
35 | | offval.7 |
. . . . 5
⊢ ((φ ∧ x ∈ B) → (𝐺‘x) = 𝐷) |
36 | 34, 35 | sylan2 270 |
. . . 4
⊢ ((φ ∧ x ∈ 𝑆) → (𝐺‘x) = 𝐷) |
37 | 31, 36 | breq12d 3768 |
. . 3
⊢ ((φ ∧ x ∈ 𝑆) → ((𝐹‘x)𝑅(𝐺‘x) ↔ 𝐶𝑅𝐷)) |
38 | 37 | ralbidva 2316 |
. 2
⊢ (φ → (∀x ∈ 𝑆 (𝐹‘x)𝑅(𝐺‘x) ↔ ∀x ∈ 𝑆 𝐶𝑅𝐷)) |
39 | 18, 26, 38 | 3bitrd 203 |
1
⊢ (φ → (𝐹 ∘𝑟 𝑅𝐺 ↔ ∀x ∈ 𝑆 𝐶𝑅𝐷)) |