Theorem cnvco 5866

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.)

Assertion

Ref	Expression
cnvco	⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)

Proof of Theorem cnvco

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		exancom 1893	. . . 4 ⊢ (∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
2		vex 3454	. . . . 5 ⊢ 𝑥 ∈ V
3		vex 3454	. . . . 5 ⊢ 𝑦 ∈ V
4	2, 3	brco 5847	. . . 4 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦))
5		vex 3454	. . . . . . 7 ⊢ 𝑧 ∈ V
6	3, 5	brcnv 5859	. . . . . 6 ⊢ (𝑦◡𝐴𝑧 ↔ 𝑧𝐴𝑦)
7	5, 2	brcnv 5859	. . . . . 6 ⊢ (𝑧◡𝐵𝑥 ↔ 𝑥𝐵𝑧)
8	6, 7	anbi12i 640	. . . . 5 ⊢ ((𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ (𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
9	8	exbii 1880	. . . 4 ⊢ (∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥) ↔ ∃𝑧(𝑧𝐴𝑦 ∧ 𝑥𝐵𝑧))
10	1, 4, 9	3bitr4i 306	. . 3 ⊢ (𝑥(𝐴 ∘ 𝐵)𝑦 ↔ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥))
11	10	opabbii 5171	. 2 ⊢ {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦} = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
12		df-cnv 5658	. 2 ⊢ ◡(𝐴 ∘ 𝐵) = {⟨𝑦, 𝑥⟩ ∣ 𝑥(𝐴 ∘ 𝐵)𝑦}
13		df-co 5659	. 2 ⊢ (◡𝐵 ∘ ◡𝐴) = {⟨𝑦, 𝑥⟩ ∣ ∃𝑧(𝑦◡𝐴𝑧 ∧ 𝑧◡𝐵𝑥)}
14	11, 12, 13	3eqtr4i 2793	1 ⊢ ◡(𝐴 ∘ 𝐵) = (◡𝐵 ∘ ◡𝐴)

This proof depends on syntax axioms:   ∧ wa 401   = wceq 1569  ∃wex 1811   class class class wbr 5102  {copab 5166  ^◡ccnv 5649   ∘ ccom 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-br 5103  df-opab 5167  df-cnv 5658  df-co 5659

This theorem is used by:  rncoss  5958  rncoeq  5962  dmco  6256  cores2  6261  co01  6263  coi2  6265  relcnvtrg  6268  relcnvtrgOLD  6269  dfdm2  6284  f1cof1  6790  cofunex2g  7962  fparlem3  8125  fparlem4  8126  suppco  8223  fsuppcolem  9393  relexpcnv  15188  relexpaddg  15206  cnvps  18752  gimco  19482  gsumzf1o  20126  rimco  20747  cnco  23584  ptrescn  23958  qtopcn  24033  hmeoco  24091  cncombf  25979  deg1val  26414  fcoinver  33198  ofpreima  33259  cycpmconjv  33703  cycpmconjs  33717  cyc3conja  33718  esplysply  34203  mbfmco  34896  eulerpartlemmf  35007  cvmliftmolem1  36046  cvmlift2lem9a  36068  cvmlift2lem9  36076  mclsppslem  36348  ftc1anclem3  38614  trlcocnv  41778  tendoicl  41854  cdlemk45  42005  cononrel1  44594  cononrel2  44595  cnvtrcl0  44626  cnvtrrel  44670  relexpaddss  44718  frege131d  44764  brco2f1o  45032  brco3f1o  45033  clsneicnv  45105  neicvgnvo  45115  cocanss1  45924  smfco  47812  upgrimpthslem1  49005  upgrimspths  49008