Step | Hyp | Ref
| Expression |
1 | | xpcomf1o.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥}) |
2 | 1 | xpcomf1o 8828 |
. . . . . . . . 9
⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) |
3 | | f1ofun 6715 |
. . . . . . . . 9
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) → Fun 𝐹) |
4 | | funbrfv2b 6822 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝑢𝐹𝑤 ↔ (𝑢 ∈ dom 𝐹 ∧ (𝐹‘𝑢) = 𝑤))) |
5 | 2, 3, 4 | mp2b 10 |
. . . . . . . 8
⊢ (𝑢𝐹𝑤 ↔ (𝑢 ∈ dom 𝐹 ∧ (𝐹‘𝑢) = 𝑤)) |
6 | | ancom 461 |
. . . . . . . 8
⊢ ((𝑢 ∈ dom 𝐹 ∧ (𝐹‘𝑢) = 𝑤) ↔ ((𝐹‘𝑢) = 𝑤 ∧ 𝑢 ∈ dom 𝐹)) |
7 | | eqcom 2747 |
. . . . . . . . 9
⊢ ((𝐹‘𝑢) = 𝑤 ↔ 𝑤 = (𝐹‘𝑢)) |
8 | | f1odm 6717 |
. . . . . . . . . . 11
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) → dom 𝐹 = (𝐴 × 𝐵)) |
9 | 2, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢ dom 𝐹 = (𝐴 × 𝐵) |
10 | 9 | eleq2i 2832 |
. . . . . . . . 9
⊢ (𝑢 ∈ dom 𝐹 ↔ 𝑢 ∈ (𝐴 × 𝐵)) |
11 | 7, 10 | anbi12i 627 |
. . . . . . . 8
⊢ (((𝐹‘𝑢) = 𝑤 ∧ 𝑢 ∈ dom 𝐹) ↔ (𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵))) |
12 | 5, 6, 11 | 3bitri 297 |
. . . . . . 7
⊢ (𝑢𝐹𝑤 ↔ (𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵))) |
13 | 12 | anbi1i 624 |
. . . . . 6
⊢ ((𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ ((𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵)) ∧ 𝑤𝐺𝑣)) |
14 | | anass 469 |
. . . . . 6
⊢ (((𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵)) ∧ 𝑤𝐺𝑣) ↔ (𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣))) |
15 | 13, 14 | bitri 274 |
. . . . 5
⊢ ((𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ (𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣))) |
16 | 15 | exbii 1854 |
. . . 4
⊢
(∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ ∃𝑤(𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣))) |
17 | | fvex 6782 |
. . . . 5
⊢ (𝐹‘𝑢) ∈ V |
18 | | breq1 5082 |
. . . . . 6
⊢ (𝑤 = (𝐹‘𝑢) → (𝑤𝐺𝑣 ↔ (𝐹‘𝑢)𝐺𝑣)) |
19 | 18 | anbi2d 629 |
. . . . 5
⊢ (𝑤 = (𝐹‘𝑢) → ((𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣) ↔ (𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣))) |
20 | 17, 19 | ceqsexv 3478 |
. . . 4
⊢
(∃𝑤(𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣)) ↔ (𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣)) |
21 | | elxp 5612 |
. . . . . 6
⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
22 | 21 | anbi1i 624 |
. . . . 5
⊢ ((𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣)) |
23 | | nfcv 2909 |
. . . . . . 7
⊢
Ⅎ𝑧(𝐹‘𝑢) |
24 | | xpcomco.1 |
. . . . . . . 8
⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) |
25 | | nfmpo2 7348 |
. . . . . . . 8
⊢
Ⅎ𝑧(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) |
26 | 24, 25 | nfcxfr 2907 |
. . . . . . 7
⊢
Ⅎ𝑧𝐺 |
27 | | nfcv 2909 |
. . . . . . 7
⊢
Ⅎ𝑧𝑣 |
28 | 23, 26, 27 | nfbr 5126 |
. . . . . 6
⊢
Ⅎ𝑧(𝐹‘𝑢)𝐺𝑣 |
29 | 28 | 19.41 2232 |
. . . . 5
⊢
(∃𝑧(∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣)) |
30 | | nfcv 2909 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝐹‘𝑢) |
31 | | nfmpo1 7347 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) |
32 | 24, 31 | nfcxfr 2907 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐺 |
33 | | nfcv 2909 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝑣 |
34 | 30, 32, 33 | nfbr 5126 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝐹‘𝑢)𝐺𝑣 |
35 | 34 | 19.41 2232 |
. . . . . . 7
⊢
(∃𝑦((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣)) |
36 | | anass 469 |
. . . . . . . . 9
⊢ (((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣))) |
37 | | fveq2 6769 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 〈𝑧, 𝑦〉 → (𝐹‘𝑢) = (𝐹‘〈𝑧, 𝑦〉)) |
38 | | opelxpi 5626 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑧, 𝑦〉 ∈ (𝐴 × 𝐵)) |
39 | | sneq 4577 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 〈𝑧, 𝑦〉 → {𝑥} = {〈𝑧, 𝑦〉}) |
40 | 39 | cnveqd 5782 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 〈𝑧, 𝑦〉 → ◡{𝑥} = ◡{〈𝑧, 𝑦〉}) |
41 | 40 | unieqd 4859 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 〈𝑧, 𝑦〉 → ∪
◡{𝑥} = ∪ ◡{〈𝑧, 𝑦〉}) |
42 | | opswap 6130 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ◡{〈𝑧, 𝑦〉} = 〈𝑦, 𝑧〉 |
43 | 41, 42 | eqtrdi 2796 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 〈𝑧, 𝑦〉 → ∪
◡{𝑥} = 〈𝑦, 𝑧〉) |
44 | | opex 5382 |
. . . . . . . . . . . . . . . 16
⊢
〈𝑦, 𝑧〉 ∈ V |
45 | 43, 1, 44 | fvmpt 6870 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑧, 𝑦〉 ∈ (𝐴 × 𝐵) → (𝐹‘〈𝑧, 𝑦〉) = 〈𝑦, 𝑧〉) |
46 | 38, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝐹‘〈𝑧, 𝑦〉) = 〈𝑦, 𝑧〉) |
47 | 37, 46 | sylan9eq 2800 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑢) = 〈𝑦, 𝑧〉) |
48 | 47 | breq1d 5089 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑢)𝐺𝑣 ↔ 〈𝑦, 𝑧〉𝐺𝑣)) |
49 | | df-br 5080 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑦, 𝑧〉𝐺𝑣 ↔ 〈〈𝑦, 𝑧〉, 𝑣〉 ∈ 𝐺) |
50 | | df-mpo 7274 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) = {〈〈𝑦, 𝑧〉, 𝑣〉 ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)} |
51 | 24, 50 | eqtri 2768 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐺 = {〈〈𝑦, 𝑧〉, 𝑣〉 ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)} |
52 | 51 | eleq2i 2832 |
. . . . . . . . . . . . . . . 16
⊢
(〈〈𝑦,
𝑧〉, 𝑣〉 ∈ 𝐺 ↔ 〈〈𝑦, 𝑧〉, 𝑣〉 ∈ {〈〈𝑦, 𝑧〉, 𝑣〉 ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)}) |
53 | | oprabidw 7300 |
. . . . . . . . . . . . . . . 16
⊢
(〈〈𝑦,
𝑧〉, 𝑣〉 ∈ {〈〈𝑦, 𝑧〉, 𝑣〉 ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)} ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)) |
54 | 49, 52, 53 | 3bitri 297 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑦, 𝑧〉𝐺𝑣 ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)) |
55 | 54 | baib 536 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) → (〈𝑦, 𝑧〉𝐺𝑣 ↔ 𝑣 = 𝐶)) |
56 | 55 | ancoms 459 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (〈𝑦, 𝑧〉𝐺𝑣 ↔ 𝑣 = 𝐶)) |
57 | 56 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (〈𝑦, 𝑧〉𝐺𝑣 ↔ 𝑣 = 𝐶)) |
58 | 48, 57 | bitrd 278 |
. . . . . . . . . . 11
⊢ ((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑢)𝐺𝑣 ↔ 𝑣 = 𝐶)) |
59 | 58 | pm5.32da 579 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑧, 𝑦〉 → (((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
60 | 59 | pm5.32i 575 |
. . . . . . . . 9
⊢ ((𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣)) ↔ (𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
61 | 36, 60 | bitri 274 |
. . . . . . . 8
⊢ (((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
62 | 61 | exbii 1854 |
. . . . . . 7
⊢
(∃𝑦((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
63 | 35, 62 | bitr3i 276 |
. . . . . 6
⊢
((∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
64 | 63 | exbii 1854 |
. . . . 5
⊢
(∃𝑧(∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
65 | 22, 29, 64 | 3bitr2i 299 |
. . . 4
⊢ ((𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
66 | 16, 20, 65 | 3bitri 297 |
. . 3
⊢
(∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
67 | 66 | opabbii 5146 |
. 2
⊢
{〈𝑢, 𝑣〉 ∣ ∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣)} = {〈𝑢, 𝑣〉 ∣ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))} |
68 | | df-co 5598 |
. 2
⊢ (𝐺 ∘ 𝐹) = {〈𝑢, 𝑣〉 ∣ ∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣)} |
69 | | df-mpo 7274 |
. . 3
⊢ (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑧, 𝑦〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} |
70 | | dfoprab2 7325 |
. . 3
⊢
{〈〈𝑧,
𝑦〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} = {〈𝑢, 𝑣〉 ∣ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))} |
71 | 69, 70 | eqtri 2768 |
. 2
⊢ (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈𝑢, 𝑣〉 ∣ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))} |
72 | 67, 68, 71 | 3eqtr4i 2778 |
1
⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |