![]() |
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 1865 | . . . 4 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧)) | |
2 | vex 3479 | . . . . 5 ⊢ 𝑥 ∈ V | |
3 | vex 3479 | . . . . 5 ⊢ 𝑦 ∈ V | |
4 | 2, 3 | brco 5871 | . . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)) |
5 | vex 3479 | . . . . . . 7 ⊢ 𝑧 ∈ V | |
6 | 3, 5 | brcnv 5883 | . . . . . 6 ⊢ (𝑦◡𝐴𝑧 ↔ 𝑧𝐴𝑦) |
7 | 5, 2 | brcnv 5883 | . . . . . 6 ⊢ (𝑧◡𝐵𝑥 ↔ 𝑥𝐵𝑧) |
8 | 6, 7 | anbi12i 628 | . . . . 5 ⊢ ((𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ (𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧)) |
9 | 8 | exbii 1851 | . . . 4 ⊢ (∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧)) |
10 | 1, 4, 9 | 3bitr4i 303 | . . 3 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)) |
11 | 10 | opabbii 5216 | . 2 ⊢ {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)} |
12 | df-cnv 5685 | . 2 ⊢ ◡(𝐴 ∘ 𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} | |
13 | df-co 5686 | . 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)} | |
14 | 11, 12, 13 | 3eqtr4i 2771 | 1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 397 = wceq 1542 ∃wex 1782 class class class wbr 5149 {copab 5211 ◡ccnv 5676 ∘ ccom 5681 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-opab 5212 df-cnv 5685 df-co 5686 |
This theorem is referenced by: rncoss 5972 rncoeq 5975 dmco 6254 cores2 6259 co01 6261 coi2 6263 relcnvtrg 6266 dfdm2 6281 f1cof1 6799 f1coOLD 6801 cofunex2g 7936 fparlem3 8100 fparlem4 8101 suppco 8191 fsuppcolem 9396 relexpcnv 14982 relexpaddg 15000 cnvps 18531 gimco 19142 gsumzf1o 19780 cnco 22770 ptrescn 23143 qtopcn 23218 hmeoco 23276 cncombf 25175 deg1val 25614 fcoinver 31835 ofpreima 31890 cycpmconjv 32301 cycpmconjs 32315 cyc3conja 32316 mbfmco 33263 eulerpartlemmf 33374 cvmliftmolem1 34272 cvmlift2lem9a 34294 cvmlift2lem9 34302 mclsppslem 34574 ftc1anclem3 36563 trlcocnv 39591 tendoicl 39667 cdlemk45 39818 rimco 41093 cononrel1 42345 cononrel2 42346 cnvtrcl0 42377 cnvtrrel 42421 relexpaddss 42469 frege131d 42515 brco2f1o 42783 brco3f1o 42784 clsneicnv 42856 neicvgnvo 42866 smfco 45518 |
Copyright terms: Public domain | W3C validator |