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 1787 | . . . 4 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧)) | |
2 | vex 3203 | . . . . 5 ⊢ 𝑥 ∈ V | |
3 | vex 3203 | . . . . 5 ⊢ 𝑦 ∈ V | |
4 | 2, 3 | brco 5292 | . . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) |
5 | vex 3203 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
6 | 3, 5 | brcnv 5305 | . . . . . 6 ⊢ (𝑦◡𝐴𝑧 ↔ 𝑧𝐴𝑦) |
7 | 5, 2 | brcnv 5305 | . . . . . 6 ⊢ (𝑧◡𝐵𝑥 ↔ 𝑥𝐵𝑧) |
8 | 6, 7 | anbi12i 733 | . . . . 5 ⊢ ((𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ (𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧)) |
9 | 8 | exbii 1774 | . . . 4 ⊢ (∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧)) |
10 | 1, 4, 9 | 3bitr4i 292 | . . 3 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)) |
11 | 10 | opabbii 4717 | . 2 ⊢ {〈𝑦, 𝑥〉 ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} = {〈𝑦, 𝑥〉 ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)} |
12 | df-cnv 5122 | . 2 ⊢ ◡(𝐴 ∘ 𝐵) = {〈𝑦, 𝑥〉 ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} | |
13 | df-co 5123 | . 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {〈𝑦, 𝑥〉 ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)} | |
14 | 11, 12, 13 | 3eqtr4i 2654 | 1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 384 = wceq 1483 ∃wex 1704 class class class wbr 4653 {copab 4712 ◡ccnv 5113 ∘ ccom 5118 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-br 4654 df-opab 4713 df-cnv 5122 df-co 5123 |
This theorem is referenced by: rncoss 5386 rncoeq 5389 dmco 5643 cores2 5648 co01 5650 coi2 5652 relcnvtr 5655 dfdm2 5667 f1co 6110 cofunex2g 7131 fparlem3 7279 fparlem4 7280 supp0cosupp0 7334 imacosupp 7335 fsuppcolem 8306 relexpcnv 13775 relexpaddg 13793 cnvps 17212 gimco 17710 gsumzf1o 18313 cnco 21070 ptrescn 21442 qtopcn 21517 hmeoco 21575 cncombf 23425 deg1val 23856 fcoinver 29418 ofpreima 29465 mbfmco 30326 eulerpartlemmf 30437 cvmliftmolem1 31263 cvmlift2lem9a 31285 cvmlift2lem9 31293 mclsppslem 31480 ftc1anclem3 33487 trlcocnv 36008 tendoicl 36084 cdlemk45 36235 cononrel1 37900 cononrel2 37901 cnvtrcl0 37933 cnvtrrel 37962 relexpaddss 38010 frege131d 38056 brco2f1o 38330 brco3f1o 38331 clsneicnv 38403 neicvgnvo 38413 smfco 41009 |
Copyright terms: Public domain | W3C validator |