![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cnvco | Structured version Visualization version GIF version |
Description: Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
Ref | Expression |
---|---|
cnvco | ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exancom 1858 | . . . 4 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧)) | |
2 | vex 3481 | . . . . 5 ⊢ 𝑥 ∈ V | |
3 | vex 3481 | . . . . 5 ⊢ 𝑦 ∈ V | |
4 | 2, 3 | brco 5883 | . . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) |
5 | vex 3481 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
6 | 3, 5 | brcnv 5895 | . . . . . 6 ⊢ (𝑦◡𝐴𝑧 ↔ 𝑧𝐴𝑦) |
7 | 5, 2 | brcnv 5895 | . . . . . 6 ⊢ (𝑧◡𝐵𝑥 ↔ 𝑥𝐵𝑧) |
8 | 6, 7 | anbi12i 628 | . . . . 5 ⊢ ((𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ (𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧)) |
9 | 8 | exbii 1844 | . . . 4 ⊢ (∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧)) |
10 | 1, 4, 9 | 3bitr4i 303 | . . 3 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)) |
11 | 10 | opabbii 5214 | . 2 ⊢ {〈𝑦, 𝑥〉 ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} = {〈𝑦, 𝑥〉 ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)} |
12 | df-cnv 5696 | . 2 ⊢ ◡(𝐴 ∘ 𝐵) = {〈𝑦, 𝑥〉 ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} | |
13 | df-co 5697 | . 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {〈𝑦, 𝑥〉 ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)} | |
14 | 11, 12, 13 | 3eqtr4i 2772 | 1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 = wceq 1536 ∃wex 1775 class class class wbr 5147 {copab 5209 ◡ccnv 5687 ∘ ccom 5692 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 ax-sep 5301 ax-nul 5311 ax-pr 5437 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5148 df-opab 5210 df-cnv 5696 df-co 5697 |
This theorem is referenced by: rncoss 5988 rncoeq 5992 dmco 6275 cores2 6280 co01 6282 coi2 6284 relcnvtrg 6287 dfdm2 6302 f1cof1 6814 cofunex2g 7972 fparlem3 8137 fparlem4 8138 suppco 8229 fsuppcolem 9438 relexpcnv 15070 relexpaddg 15088 cnvps 18635 gimco 19298 gsumzf1o 19944 cnco 23289 ptrescn 23662 qtopcn 23737 hmeoco 23795 cncombf 25706 deg1val 26149 fcoinver 32623 ofpreima 32681 cycpmconjv 33144 cycpmconjs 33158 cyc3conja 33159 mbfmco 34245 eulerpartlemmf 34356 cvmliftmolem1 35265 cvmlift2lem9a 35287 cvmlift2lem9 35295 mclsppslem 35567 ftc1anclem3 37681 trlcocnv 40702 tendoicl 40778 cdlemk45 40929 rimco 42504 cononrel1 43583 cononrel2 43584 cnvtrcl0 43615 cnvtrrel 43659 relexpaddss 43707 frege131d 43753 brco2f1o 44021 brco3f1o 44022 clsneicnv 44094 neicvgnvo 44104 smfco 46757 |
Copyright terms: Public domain | W3C validator |