| Step | Hyp | Ref
| Expression |
| 1 | | xpcomf1o.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ (𝐴 × 𝐵) ↦ ∪ ◡{𝑥}) |
| 2 | 1 | xpcomf1o 9101 |
. . . . . . . . 9
⊢ 𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) |
| 3 | | f1ofun 6850 |
. . . . . . . . 9
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) → Fun 𝐹) |
| 4 | | funbrfv2b 6966 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝑢𝐹𝑤 ↔ (𝑢 ∈ dom 𝐹 ∧ (𝐹‘𝑢) = 𝑤))) |
| 5 | 2, 3, 4 | mp2b 10 |
. . . . . . . 8
⊢ (𝑢𝐹𝑤 ↔ (𝑢 ∈ dom 𝐹 ∧ (𝐹‘𝑢) = 𝑤)) |
| 6 | | ancom 460 |
. . . . . . . 8
⊢ ((𝑢 ∈ dom 𝐹 ∧ (𝐹‘𝑢) = 𝑤) ↔ ((𝐹‘𝑢) = 𝑤 ∧ 𝑢 ∈ dom 𝐹)) |
| 7 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝐹‘𝑢) = 𝑤 ↔ 𝑤 = (𝐹‘𝑢)) |
| 8 | | f1odm 6852 |
. . . . . . . . . . 11
⊢ (𝐹:(𝐴 × 𝐵)–1-1-onto→(𝐵 × 𝐴) → dom 𝐹 = (𝐴 × 𝐵)) |
| 9 | 2, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢ dom 𝐹 = (𝐴 × 𝐵) |
| 10 | 9 | eleq2i 2833 |
. . . . . . . . 9
⊢ (𝑢 ∈ dom 𝐹 ↔ 𝑢 ∈ (𝐴 × 𝐵)) |
| 11 | 7, 10 | anbi12i 628 |
. . . . . . . 8
⊢ (((𝐹‘𝑢) = 𝑤 ∧ 𝑢 ∈ dom 𝐹) ↔ (𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵))) |
| 12 | 5, 6, 11 | 3bitri 297 |
. . . . . . 7
⊢ (𝑢𝐹𝑤 ↔ (𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵))) |
| 13 | 12 | anbi1i 624 |
. . . . . 6
⊢ ((𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ ((𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵)) ∧ 𝑤𝐺𝑣)) |
| 14 | | anass 468 |
. . . . . 6
⊢ (((𝑤 = (𝐹‘𝑢) ∧ 𝑢 ∈ (𝐴 × 𝐵)) ∧ 𝑤𝐺𝑣) ↔ (𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣))) |
| 15 | 13, 14 | bitri 275 |
. . . . 5
⊢ ((𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ (𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣))) |
| 16 | 15 | exbii 1848 |
. . . 4
⊢
(∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ ∃𝑤(𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣))) |
| 17 | | fvex 6919 |
. . . . 5
⊢ (𝐹‘𝑢) ∈ V |
| 18 | | breq1 5146 |
. . . . . 6
⊢ (𝑤 = (𝐹‘𝑢) → (𝑤𝐺𝑣 ↔ (𝐹‘𝑢)𝐺𝑣)) |
| 19 | 18 | anbi2d 630 |
. . . . 5
⊢ (𝑤 = (𝐹‘𝑢) → ((𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣) ↔ (𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣))) |
| 20 | 17, 19 | ceqsexv 3532 |
. . . 4
⊢
(∃𝑤(𝑤 = (𝐹‘𝑢) ∧ (𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑤𝐺𝑣)) ↔ (𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣)) |
| 21 | | elxp 5708 |
. . . . . 6
⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))) |
| 22 | 21 | anbi1i 624 |
. . . . 5
⊢ ((𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣)) |
| 23 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑧(𝐹‘𝑢) |
| 24 | | xpcomco.1 |
. . . . . . . 8
⊢ 𝐺 = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) |
| 25 | | nfmpo2 7514 |
. . . . . . . 8
⊢
Ⅎ𝑧(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) |
| 26 | 24, 25 | nfcxfr 2903 |
. . . . . . 7
⊢
Ⅎ𝑧𝐺 |
| 27 | | nfcv 2905 |
. . . . . . 7
⊢
Ⅎ𝑧𝑣 |
| 28 | 23, 26, 27 | nfbr 5190 |
. . . . . 6
⊢
Ⅎ𝑧(𝐹‘𝑢)𝐺𝑣 |
| 29 | 28 | 19.41 2235 |
. . . . 5
⊢
(∃𝑧(∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣)) |
| 30 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑦(𝐹‘𝑢) |
| 31 | | nfmpo1 7513 |
. . . . . . . . . 10
⊢
Ⅎ𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) |
| 32 | 24, 31 | nfcxfr 2903 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝐺 |
| 33 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑦𝑣 |
| 34 | 30, 32, 33 | nfbr 5190 |
. . . . . . . 8
⊢
Ⅎ𝑦(𝐹‘𝑢)𝐺𝑣 |
| 35 | 34 | 19.41 2235 |
. . . . . . 7
⊢
(∃𝑦((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣)) |
| 36 | | anass 468 |
. . . . . . . . 9
⊢ (((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣))) |
| 37 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 〈𝑧, 𝑦〉 → (𝐹‘𝑢) = (𝐹‘〈𝑧, 𝑦〉)) |
| 38 | | opelxpi 5722 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑧, 𝑦〉 ∈ (𝐴 × 𝐵)) |
| 39 | | sneq 4636 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 〈𝑧, 𝑦〉 → {𝑥} = {〈𝑧, 𝑦〉}) |
| 40 | 39 | cnveqd 5886 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 〈𝑧, 𝑦〉 → ◡{𝑥} = ◡{〈𝑧, 𝑦〉}) |
| 41 | 40 | unieqd 4920 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 〈𝑧, 𝑦〉 → ∪
◡{𝑥} = ∪ ◡{〈𝑧, 𝑦〉}) |
| 42 | | opswap 6249 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ ◡{〈𝑧, 𝑦〉} = 〈𝑦, 𝑧〉 |
| 43 | 41, 42 | eqtrdi 2793 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 〈𝑧, 𝑦〉 → ∪
◡{𝑥} = 〈𝑦, 𝑧〉) |
| 44 | | opex 5469 |
. . . . . . . . . . . . . . . 16
⊢
〈𝑦, 𝑧〉 ∈ V |
| 45 | 43, 1, 44 | fvmpt 7016 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑧, 𝑦〉 ∈ (𝐴 × 𝐵) → (𝐹‘〈𝑧, 𝑦〉) = 〈𝑦, 𝑧〉) |
| 46 | 38, 45 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (𝐹‘〈𝑧, 𝑦〉) = 〈𝑦, 𝑧〉) |
| 47 | 37, 46 | sylan9eq 2797 |
. . . . . . . . . . . . 13
⊢ ((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘𝑢) = 〈𝑦, 𝑧〉) |
| 48 | 47 | breq1d 5153 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑢)𝐺𝑣 ↔ 〈𝑦, 𝑧〉𝐺𝑣)) |
| 49 | | df-br 5144 |
. . . . . . . . . . . . . . . 16
⊢
(〈𝑦, 𝑧〉𝐺𝑣 ↔ 〈〈𝑦, 𝑧〉, 𝑣〉 ∈ 𝐺) |
| 50 | | df-mpo 7436 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐴 ↦ 𝐶) = {〈〈𝑦, 𝑧〉, 𝑣〉 ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)} |
| 51 | 24, 50 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
⊢ 𝐺 = {〈〈𝑦, 𝑧〉, 𝑣〉 ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)} |
| 52 | 51 | eleq2i 2833 |
. . . . . . . . . . . . . . . 16
⊢
(〈〈𝑦,
𝑧〉, 𝑣〉 ∈ 𝐺 ↔ 〈〈𝑦, 𝑧〉, 𝑣〉 ∈ {〈〈𝑦, 𝑧〉, 𝑣〉 ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)}) |
| 53 | | oprabidw 7462 |
. . . . . . . . . . . . . . . 16
⊢
(〈〈𝑦,
𝑧〉, 𝑣〉 ∈ {〈〈𝑦, 𝑧〉, 𝑣〉 ∣ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)} ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)) |
| 54 | 49, 52, 53 | 3bitri 297 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑦, 𝑧〉𝐺𝑣 ↔ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) ∧ 𝑣 = 𝐶)) |
| 55 | 54 | baib 535 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴) → (〈𝑦, 𝑧〉𝐺𝑣 ↔ 𝑣 = 𝐶)) |
| 56 | 55 | ancoms 458 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (〈𝑦, 𝑧〉𝐺𝑣 ↔ 𝑣 = 𝐶)) |
| 57 | 56 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (〈𝑦, 𝑧〉𝐺𝑣 ↔ 𝑣 = 𝐶)) |
| 58 | 48, 57 | bitrd 279 |
. . . . . . . . . . 11
⊢ ((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ((𝐹‘𝑢)𝐺𝑣 ↔ 𝑣 = 𝐶)) |
| 59 | 58 | pm5.32da 579 |
. . . . . . . . . 10
⊢ (𝑢 = 〈𝑧, 𝑦〉 → (((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
| 60 | 59 | pm5.32i 574 |
. . . . . . . . 9
⊢ ((𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣)) ↔ (𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
| 61 | 36, 60 | bitri 275 |
. . . . . . . 8
⊢ (((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ (𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
| 62 | 61 | exbii 1848 |
. . . . . . 7
⊢
(∃𝑦((𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
| 63 | 35, 62 | bitr3i 277 |
. . . . . 6
⊢
((∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
| 64 | 63 | exbii 1848 |
. . . . 5
⊢
(∃𝑧(∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ (𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
| 65 | 22, 29, 64 | 3bitr2i 299 |
. . . 4
⊢ ((𝑢 ∈ (𝐴 × 𝐵) ∧ (𝐹‘𝑢)𝐺𝑣) ↔ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
| 66 | 16, 20, 65 | 3bitri 297 |
. . 3
⊢
(∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣) ↔ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))) |
| 67 | 66 | opabbii 5210 |
. 2
⊢
{〈𝑢, 𝑣〉 ∣ ∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣)} = {〈𝑢, 𝑣〉 ∣ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))} |
| 68 | | df-co 5694 |
. 2
⊢ (𝐺 ∘ 𝐹) = {〈𝑢, 𝑣〉 ∣ ∃𝑤(𝑢𝐹𝑤 ∧ 𝑤𝐺𝑣)} |
| 69 | | df-mpo 7436 |
. . 3
⊢ (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑧, 𝑦〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} |
| 70 | | dfoprab2 7491 |
. . 3
⊢
{〈〈𝑧,
𝑦〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} = {〈𝑢, 𝑣〉 ∣ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))} |
| 71 | 69, 70 | eqtri 2765 |
. 2
⊢ (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈𝑢, 𝑣〉 ∣ ∃𝑧∃𝑦(𝑢 = 〈𝑧, 𝑦〉 ∧ ((𝑧 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶))} |
| 72 | 67, 68, 71 | 3eqtr4i 2775 |
1
⊢ (𝐺 ∘ 𝐹) = (𝑧 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) |