Step | Hyp | Ref
| Expression |
1 | | xpcomf1o.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥}) |
2 | 1 | xpcomf1o 9012 |
. . . . . . . . 9
⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) |
3 | | f1ofun 6791 |
. . . . . . . . 9
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) → Fun 𝐹) |
4 | | funbrfv2b 6905 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝑢𝐹𝑤 ↔ (𝑢 ∈ dom 𝐹 ∧ (𝐹‘𝑢) = 𝑤))) |
5 | 2, 3, 4 | mp2b 10 |
. . . . . . . 8
⊢ (𝑢𝐹𝑤 ↔ (𝑢 ∈ dom 𝐹 ∧ (𝐹‘𝑢) = 𝑤)) |
6 | | ancom 462 |
. . . . . . . 8
⊢ ((𝑢 ∈ dom 𝐹 ∧ (𝐹‘𝑢) = 𝑤) ↔ ((𝐹‘𝑢) = 𝑤 ∧ 𝑢 ∈ dom 𝐹)) |
7 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝐹‘𝑢) = 𝑤 ↔ 𝑤 = (𝐹‘𝑢)) |
8 | | f1odm 6793 |
. . . . . . . . . . 11
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) → dom 𝐹 = (𝐴 × 𝐵)) |
9 | 2, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢ dom 𝐹 = (𝐴 × 𝐵) |
10 | 9 | eleq2i 2830 |
. . . . . . . . 9
⊢ (𝑢 ∈ dom 𝐹 ↔ 𝑢 ∈ (𝐴 × 𝐵)) |
11 | 7, 10 | anbi12i 628 |
. . . . . . . 8
⊢ (((𝐹‘𝑢) = 𝑤 ∧ 𝑢 ∈ dom 𝐹) ↔ (𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵))) |
12 | 5, 6, 11 | 3bitri 297 |
. . . . . . 7
⊢ (𝑢𝐹𝑤 ↔ (𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵))) |
13 | 12 | anbi1i 625 |
. . . . . 6
⊢ ((𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ ((𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵)) ∧ 𝑤𝐺𝑣)) |
14 | | anass 470 |
. . . . . 6
⊢ (((𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵)) ∧ 𝑤𝐺𝑣) ↔ (𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣))) |
15 | 13, 14 | bitri 275 |
. . . . 5
⊢ ((𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ (𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣))) |
16 | 15 | exbii 1851 |
. . . 4
⊢
(∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ ∃𝑤(𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣))) |
17 | | fvex 6860 |
. . . . 5
⊢ (𝐹‘𝑢) ∈ V |
18 | | breq1 5113 |
. . . . . 6
⊢ (𝑤 = (𝐹‘𝑢) → (𝑤𝐺𝑣 ↔ (𝐹‘𝑢)𝐺𝑣)) |
19 | 18 | anbi2d 630 |
. . . . 5
⊢ (𝑤 = (𝐹‘𝑢) → ((𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣) ↔ (𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣))) |
20 | 17, 19 | ceqsexv 3497 |
. . . 4
⊢
(∃𝑤(𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣)) ↔ (𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣)) |
21 | | elxp 5661 |
. . . . . 6
⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑧∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
22 | 21 | anbi1i 625 |
. . . . 5
⊢ ((𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (∃𝑧∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣)) |
23 | | nfcv 2908 |
. . . . . . 7
⊢
Ⅎ𝑧(𝐹‘𝑢) |
24 | | xpcomco.1 |
. . . . . . . 8
⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) |
25 | | nfmpo2 7443 |
. . . . . . . 8
⊢
Ⅎ𝑧(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) |
26 | 24, 25 | nfcxfr 2906 |
. . . . . . 7
⊢
Ⅎ𝑧𝐺 |
27 | | nfcv 2908 |
. . . . . . 7
⊢
Ⅎ𝑧𝑣 |
28 | 23, 26, 27 | nfbr 5157 |
. . . . . 6
⊢
Ⅎ𝑧(𝐹‘𝑢)𝐺𝑣 |
29 | 28 | 19.41 2229 |
. . . . 5
⊢
(∃𝑧(∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (∃𝑧∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣)) |
30 | | nfcv 2908 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝐹‘𝑢) |
31 | | nfmpo1 7442 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) |
32 | 24, 31 | nfcxfr 2906 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐺 |
33 | | nfcv 2908 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝑣 |
34 | 30, 32, 33 | nfbr 5157 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝐹‘𝑢)𝐺𝑣 |
35 | 34 | 19.41 2229 |
. . . . . . 7
⊢
(∃𝑦((𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣)) |
36 | | anass 470 |
. . . . . . . . 9
⊢ (((𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣))) |
37 | | fveq2 6847 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = ⟨𝑧, 𝑦⟩ → (𝐹‘𝑢) = (𝐹‘⟨𝑧, 𝑦⟩)) |
38 | | opelxpi 5675 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → ⟨𝑧, 𝑦⟩ ∈ (𝐴 × 𝐵)) |
39 | | sneq 4601 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = ⟨𝑧, 𝑦⟩ → {𝑥} = {⟨𝑧, 𝑦⟩}) |
40 | 39 | cnveqd 5836 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = ⟨𝑧, 𝑦⟩ → ◡{𝑥} = ◡{⟨𝑧, 𝑦⟩}) |
41 | 40 | unieqd 4884 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = ⟨𝑧, 𝑦⟩ → ∪
◡{𝑥} = ∪ ◡{⟨𝑧, 𝑦⟩}) |
42 | | opswap 6186 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ◡{⟨𝑧, 𝑦⟩} = ⟨𝑦, 𝑧⟩ |
43 | 41, 42 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ⟨𝑧, 𝑦⟩ → ∪
◡{𝑥} = ⟨𝑦, 𝑧⟩) |
44 | | opex 5426 |
. . . . . . . . . . . . . . . 16
⊢
⟨𝑦, 𝑧⟩ ∈ V |
45 | 43, 1, 44 | fvmpt 6953 |
. . . . . . . . . . . . . . 15
⊢
(⟨𝑧, 𝑦⟩ ∈ (𝐴 × 𝐵) → (𝐹‘⟨𝑧, 𝑦⟩) = ⟨𝑦, 𝑧⟩) |
46 | 38, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝐹‘⟨𝑧, 𝑦⟩) = ⟨𝑦, 𝑧⟩) |
47 | 37, 46 | sylan9eq 2797 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑢) = ⟨𝑦, 𝑧⟩) |
48 | 47 | breq1d 5120 |
. . . . . . . . . . . 12
⊢ ((𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑢)𝐺𝑣 ↔ ⟨𝑦, 𝑧⟩𝐺𝑣)) |
49 | | df-br 5111 |
. . . . . . . . . . . . . . . 16
⊢
(⟨𝑦, 𝑧⟩𝐺𝑣 ↔ ⟨⟨𝑦, 𝑧⟩, 𝑣⟩ ∈ 𝐺) |
50 | | df-mpo 7367 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) = {⟨⟨𝑦, 𝑧⟩, 𝑣⟩ ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)} |
51 | 24, 50 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐺 = {⟨⟨𝑦, 𝑧⟩, 𝑣⟩ ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)} |
52 | 51 | eleq2i 2830 |
. . . . . . . . . . . . . . . 16
⊢
(⟨⟨𝑦,
𝑧⟩, 𝑣⟩ ∈ 𝐺 ↔ ⟨⟨𝑦, 𝑧⟩, 𝑣⟩ ∈ {⟨⟨𝑦, 𝑧⟩, 𝑣⟩ ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)}) |
53 | | oprabidw 7393 |
. . . . . . . . . . . . . . . 16
⊢
(⟨⟨𝑦,
𝑧⟩, 𝑣⟩ ∈ {⟨⟨𝑦, 𝑧⟩, 𝑣⟩ ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)} ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)) |
54 | 49, 52, 53 | 3bitri 297 |
. . . . . . . . . . . . . . 15
⊢
(⟨𝑦, 𝑧⟩𝐺𝑣 ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)) |
55 | 54 | baib 537 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) → (⟨𝑦, 𝑧⟩𝐺𝑣 ↔ 𝑣 = 𝐶)) |
56 | 55 | ancoms 460 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (⟨𝑦, 𝑧⟩𝐺𝑣 ↔ 𝑣 = 𝐶)) |
57 | 56 | adantl 483 |
. . . . . . . . . . . 12
⊢ ((𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (⟨𝑦, 𝑧⟩𝐺𝑣 ↔ 𝑣 = 𝐶)) |
58 | 48, 57 | bitrd 279 |
. . . . . . . . . . 11
⊢ ((𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑢)𝐺𝑣 ↔ 𝑣 = 𝐶)) |
59 | 58 | pm5.32da 580 |
. . . . . . . . . 10
⊢ (𝑢 = ⟨𝑧, 𝑦⟩ → (((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
60 | 59 | pm5.32i 576 |
. . . . . . . . 9
⊢ ((𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣)) ↔ (𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
61 | 36, 60 | bitri 275 |
. . . . . . . 8
⊢ (((𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
62 | 61 | exbii 1851 |
. . . . . . 7
⊢
(∃𝑦((𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
63 | 35, 62 | bitr3i 277 |
. . . . . 6
⊢
((∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
64 | 63 | exbii 1851 |
. . . . 5
⊢
(∃𝑧(∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑧∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
65 | 22, 29, 64 | 3bitr2i 299 |
. . . 4
⊢ ((𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑧∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
66 | 16, 20, 65 | 3bitri 297 |
. . 3
⊢
(∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ ∃𝑧∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
67 | 66 | opabbii 5177 |
. 2
⊢
{⟨𝑢, 𝑣⟩ ∣ ∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣)} = {⟨𝑢, 𝑣⟩ ∣ ∃𝑧∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))} |
68 | | df-co 5647 |
. 2
⊢ (𝐺 ∘ 𝐹) = {⟨𝑢, 𝑣⟩ ∣ ∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣)} |
69 | | df-mpo 7367 |
. . 3
⊢ (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨⟨𝑧, 𝑦⟩, 𝑣⟩ ∣ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} |
70 | | dfoprab2 7420 |
. . 3
⊢
{⟨⟨𝑧,
𝑦⟩, 𝑣⟩ ∣ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} = {⟨𝑢, 𝑣⟩ ∣ ∃𝑧∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))} |
71 | 69, 70 | eqtri 2765 |
. 2
⊢ (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {⟨𝑢, 𝑣⟩ ∣ ∃𝑧∃𝑦(𝑢 = ⟨𝑧, 𝑦⟩ ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))} |
72 | 67, 68, 71 | 3eqtr4i 2775 |
1
⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |