Step | Hyp | Ref
| Expression |
1 | | nfmpt1 5021 |
. . . . . . 7
⊢
Ⅎ𝑠(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) |
2 | | ofpreima.1 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
3 | | ofpreima.2 |
. . . . . . 7
⊢ (𝜑 → 𝐺:𝐴⟶𝐶) |
4 | | ofpreima.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | | eqidd 2773 |
. . . . . . 7
⊢ (𝜑 → (𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) = (𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)) |
6 | | ofpreima.4 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 Fn (𝐵 × 𝐶)) |
7 | | fnov 7096 |
. . . . . . . 8
⊢ (𝑅 Fn (𝐵 × 𝐶) ↔ 𝑅 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))) |
8 | 6, 7 | sylib 210 |
. . . . . . 7
⊢ (𝜑 → 𝑅 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐶 ↦ (𝑥𝑅𝑦))) |
9 | 1, 2, 3, 4, 5, 8 | ofoprabco 30185 |
. . . . . 6
⊢ (𝜑 → (𝐹 ∘𝑓 𝑅𝐺) = (𝑅 ∘ (𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉))) |
10 | 9 | cnveqd 5592 |
. . . . 5
⊢ (𝜑 → ◡(𝐹 ∘𝑓 𝑅𝐺) = ◡(𝑅 ∘ (𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉))) |
11 | | cnvco 5602 |
. . . . 5
⊢ ◡(𝑅 ∘ (𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)) = (◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) ∘ ◡𝑅) |
12 | 10, 11 | syl6eq 2824 |
. . . 4
⊢ (𝜑 → ◡(𝐹 ∘𝑓 𝑅𝐺) = (◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) ∘ ◡𝑅)) |
13 | 12 | imaeq1d 5766 |
. . 3
⊢ (𝜑 → (◡(𝐹 ∘𝑓 𝑅𝐺) “ 𝐷) = ((◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) ∘ ◡𝑅) “ 𝐷)) |
14 | | imaco 5940 |
. . 3
⊢ ((◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) ∘ ◡𝑅) “ 𝐷) = (◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) “ (◡𝑅 “ 𝐷)) |
15 | 13, 14 | syl6eq 2824 |
. 2
⊢ (𝜑 → (◡(𝐹 ∘𝑓 𝑅𝐺) “ 𝐷) = (◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) “ (◡𝑅 “ 𝐷))) |
16 | | dfima2 5769 |
. . 3
⊢ (◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) “ (◡𝑅 “ 𝐷)) = {𝑞 ∣ ∃𝑝 ∈ (◡𝑅 “ 𝐷)𝑝◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)𝑞} |
17 | | vex 3412 |
. . . . . . . 8
⊢ 𝑝 ∈ V |
18 | | vex 3412 |
. . . . . . . 8
⊢ 𝑞 ∈ V |
19 | 17, 18 | brcnv 5599 |
. . . . . . 7
⊢ (𝑝◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)𝑞 ↔ 𝑞(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)𝑝) |
20 | | funmpt 6223 |
. . . . . . . . 9
⊢ Fun
(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) |
21 | | funbrfv2b 6550 |
. . . . . . . . 9
⊢ (Fun
(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) → (𝑞(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)𝑝 ↔ (𝑞 ∈ dom (𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) ∧ ((𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)‘𝑞) = 𝑝))) |
22 | 20, 21 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑞(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)𝑝 ↔ (𝑞 ∈ dom (𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) ∧ ((𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)‘𝑞) = 𝑝)) |
23 | | opex 5209 |
. . . . . . . . . . 11
⊢
〈(𝐹‘𝑠), (𝐺‘𝑠)〉 ∈ V |
24 | | eqid 2772 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) = (𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) |
25 | 23, 24 | dmmpti 6319 |
. . . . . . . . . 10
⊢ dom
(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) = 𝐴 |
26 | 25 | eleq2i 2851 |
. . . . . . . . 9
⊢ (𝑞 ∈ dom (𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) ↔ 𝑞 ∈ 𝐴) |
27 | 26 | anbi1i 614 |
. . . . . . . 8
⊢ ((𝑞 ∈ dom (𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) ∧ ((𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)‘𝑞) = 𝑝) ↔ (𝑞 ∈ 𝐴 ∧ ((𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)‘𝑞) = 𝑝)) |
28 | 22, 27 | bitri 267 |
. . . . . . 7
⊢ (𝑞(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)𝑝 ↔ (𝑞 ∈ 𝐴 ∧ ((𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)‘𝑞) = 𝑝)) |
29 | | fveq2 6496 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑞 → (𝐹‘𝑠) = (𝐹‘𝑞)) |
30 | | fveq2 6496 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝑞 → (𝐺‘𝑠) = (𝐺‘𝑞)) |
31 | 29, 30 | opeq12d 4681 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑞 → 〈(𝐹‘𝑠), (𝐺‘𝑠)〉 = 〈(𝐹‘𝑞), (𝐺‘𝑞)〉) |
32 | | opex 5209 |
. . . . . . . . . 10
⊢
〈(𝐹‘𝑞), (𝐺‘𝑞)〉 ∈ V |
33 | 31, 24, 32 | fvmpt 6593 |
. . . . . . . . 9
⊢ (𝑞 ∈ 𝐴 → ((𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)‘𝑞) = 〈(𝐹‘𝑞), (𝐺‘𝑞)〉) |
34 | 33 | eqeq1d 2774 |
. . . . . . . 8
⊢ (𝑞 ∈ 𝐴 → (((𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)‘𝑞) = 𝑝 ↔ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝)) |
35 | 34 | pm5.32i 567 |
. . . . . . 7
⊢ ((𝑞 ∈ 𝐴 ∧ ((𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)‘𝑞) = 𝑝) ↔ (𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝)) |
36 | 19, 28, 35 | 3bitri 289 |
. . . . . 6
⊢ (𝑝◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)𝑞 ↔ (𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝)) |
37 | 36 | rexbii 3188 |
. . . . 5
⊢
(∃𝑝 ∈
(◡𝑅 “ 𝐷)𝑝◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)𝑞 ↔ ∃𝑝 ∈ (◡𝑅 “ 𝐷)(𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝)) |
38 | 37 | abbii 2838 |
. . . 4
⊢ {𝑞 ∣ ∃𝑝 ∈ (◡𝑅 “ 𝐷)𝑝◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)𝑞} = {𝑞 ∣ ∃𝑝 ∈ (◡𝑅 “ 𝐷)(𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝)} |
39 | | nfv 1873 |
. . . . 5
⊢
Ⅎ𝑞𝜑 |
40 | | nfab1 2928 |
. . . . 5
⊢
Ⅎ𝑞{𝑞 ∣ ∃𝑝 ∈ (◡𝑅 “ 𝐷)(𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝)} |
41 | | nfcv 2926 |
. . . . 5
⊢
Ⅎ𝑞∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) |
42 | | eliun 4792 |
. . . . . 6
⊢ (𝑞 ∈ ∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ↔ ∃𝑝 ∈ (◡𝑅 “ 𝐷)𝑞 ∈ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
43 | | ffn 6341 |
. . . . . . . . . . . . 13
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
44 | | fniniseg 6653 |
. . . . . . . . . . . . 13
⊢ (𝐹 Fn 𝐴 → (𝑞 ∈ (◡𝐹 “ {(1st ‘𝑝)}) ↔ (𝑞 ∈ 𝐴 ∧ (𝐹‘𝑞) = (1st ‘𝑝)))) |
45 | 2, 43, 44 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑞 ∈ (◡𝐹 “ {(1st ‘𝑝)}) ↔ (𝑞 ∈ 𝐴 ∧ (𝐹‘𝑞) = (1st ‘𝑝)))) |
46 | | ffn 6341 |
. . . . . . . . . . . . 13
⊢ (𝐺:𝐴⟶𝐶 → 𝐺 Fn 𝐴) |
47 | | fniniseg 6653 |
. . . . . . . . . . . . 13
⊢ (𝐺 Fn 𝐴 → (𝑞 ∈ (◡𝐺 “ {(2nd ‘𝑝)}) ↔ (𝑞 ∈ 𝐴 ∧ (𝐺‘𝑞) = (2nd ‘𝑝)))) |
48 | 3, 46, 47 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑞 ∈ (◡𝐺 “ {(2nd ‘𝑝)}) ↔ (𝑞 ∈ 𝐴 ∧ (𝐺‘𝑞) = (2nd ‘𝑝)))) |
49 | 45, 48 | anbi12d 621 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑞 ∈ (◡𝐹 “ {(1st ‘𝑝)}) ∧ 𝑞 ∈ (◡𝐺 “ {(2nd ‘𝑝)})) ↔ ((𝑞 ∈ 𝐴 ∧ (𝐹‘𝑞) = (1st ‘𝑝)) ∧ (𝑞 ∈ 𝐴 ∧ (𝐺‘𝑞) = (2nd ‘𝑝))))) |
50 | | elin 4051 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ↔ (𝑞 ∈ (◡𝐹 “ {(1st ‘𝑝)}) ∧ 𝑞 ∈ (◡𝐺 “ {(2nd ‘𝑝)}))) |
51 | | anandi 663 |
. . . . . . . . . . 11
⊢ ((𝑞 ∈ 𝐴 ∧ ((𝐹‘𝑞) = (1st ‘𝑝) ∧ (𝐺‘𝑞) = (2nd ‘𝑝))) ↔ ((𝑞 ∈ 𝐴 ∧ (𝐹‘𝑞) = (1st ‘𝑝)) ∧ (𝑞 ∈ 𝐴 ∧ (𝐺‘𝑞) = (2nd ‘𝑝)))) |
52 | 49, 50, 51 | 3bitr4g 306 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑞 ∈ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ↔ (𝑞 ∈ 𝐴 ∧ ((𝐹‘𝑞) = (1st ‘𝑝) ∧ (𝐺‘𝑞) = (2nd ‘𝑝))))) |
53 | 52 | adantr 473 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (◡𝑅 “ 𝐷)) → (𝑞 ∈ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ↔ (𝑞 ∈ 𝐴 ∧ ((𝐹‘𝑞) = (1st ‘𝑝) ∧ (𝐺‘𝑞) = (2nd ‘𝑝))))) |
54 | | cnvimass 5786 |
. . . . . . . . . . . . . 14
⊢ (◡𝑅 “ 𝐷) ⊆ dom 𝑅 |
55 | | fndm 6285 |
. . . . . . . . . . . . . . 15
⊢ (𝑅 Fn (𝐵 × 𝐶) → dom 𝑅 = (𝐵 × 𝐶)) |
56 | 6, 55 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom 𝑅 = (𝐵 × 𝐶)) |
57 | 54, 56 | syl5sseq 3903 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (◡𝑅 “ 𝐷) ⊆ (𝐵 × 𝐶)) |
58 | 57 | sselda 3852 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ (◡𝑅 “ 𝐷)) → 𝑝 ∈ (𝐵 × 𝐶)) |
59 | | 1st2nd2 7538 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ (𝐵 × 𝐶) → 𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
60 | | eqeq2 2783 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉 →
(〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝 ↔ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉)) |
61 | 58, 59, 60 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ (◡𝑅 “ 𝐷)) → (〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝 ↔ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉)) |
62 | | fvex 6509 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑞) ∈ V |
63 | | fvex 6509 |
. . . . . . . . . . . 12
⊢ (𝐺‘𝑞) ∈ V |
64 | 62, 63 | opth 5221 |
. . . . . . . . . . 11
⊢
(〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉 ↔ ((𝐹‘𝑞) = (1st ‘𝑝) ∧ (𝐺‘𝑞) = (2nd ‘𝑝))) |
65 | 61, 64 | syl6bb 279 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ (◡𝑅 “ 𝐷)) → (〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝 ↔ ((𝐹‘𝑞) = (1st ‘𝑝) ∧ (𝐺‘𝑞) = (2nd ‘𝑝)))) |
66 | 65 | anbi2d 619 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ (◡𝑅 “ 𝐷)) → ((𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝) ↔ (𝑞 ∈ 𝐴 ∧ ((𝐹‘𝑞) = (1st ‘𝑝) ∧ (𝐺‘𝑞) = (2nd ‘𝑝))))) |
67 | 53, 66 | bitr4d 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ (◡𝑅 “ 𝐷)) → (𝑞 ∈ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ↔ (𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝))) |
68 | 67 | rexbidva 3235 |
. . . . . . 7
⊢ (𝜑 → (∃𝑝 ∈ (◡𝑅 “ 𝐷)𝑞 ∈ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ↔ ∃𝑝 ∈ (◡𝑅 “ 𝐷)(𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝))) |
69 | | abid 2756 |
. . . . . . 7
⊢ (𝑞 ∈ {𝑞 ∣ ∃𝑝 ∈ (◡𝑅 “ 𝐷)(𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝)} ↔ ∃𝑝 ∈ (◡𝑅 “ 𝐷)(𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝)) |
70 | 68, 69 | syl6bbr 281 |
. . . . . 6
⊢ (𝜑 → (∃𝑝 ∈ (◡𝑅 “ 𝐷)𝑞 ∈ ((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})) ↔ 𝑞 ∈ {𝑞 ∣ ∃𝑝 ∈ (◡𝑅 “ 𝐷)(𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝)})) |
71 | 42, 70 | syl5rbb 276 |
. . . . 5
⊢ (𝜑 → (𝑞 ∈ {𝑞 ∣ ∃𝑝 ∈ (◡𝑅 “ 𝐷)(𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝)} ↔ 𝑞 ∈ ∪
𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)})))) |
72 | 39, 40, 41, 71 | eqrd 3871 |
. . . 4
⊢ (𝜑 → {𝑞 ∣ ∃𝑝 ∈ (◡𝑅 “ 𝐷)(𝑞 ∈ 𝐴 ∧ 〈(𝐹‘𝑞), (𝐺‘𝑞)〉 = 𝑝)} = ∪
𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
73 | 38, 72 | syl5eq 2820 |
. . 3
⊢ (𝜑 → {𝑞 ∣ ∃𝑝 ∈ (◡𝑅 “ 𝐷)𝑝◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉)𝑞} = ∪ 𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
74 | 16, 73 | syl5eq 2820 |
. 2
⊢ (𝜑 → (◡(𝑠 ∈ 𝐴 ↦ 〈(𝐹‘𝑠), (𝐺‘𝑠)〉) “ (◡𝑅 “ 𝐷)) = ∪
𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |
75 | 15, 74 | eqtrd 2808 |
1
⊢ (𝜑 → (◡(𝐹 ∘𝑓 𝑅𝐺) “ 𝐷) = ∪
𝑝 ∈ (◡𝑅 “ 𝐷)((◡𝐹 “ {(1st ‘𝑝)}) ∩ (◡𝐺 “ {(2nd ‘𝑝)}))) |