Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  co02 Structured version   Visualization version   GIF version

Theorem co02 6094
 Description: Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.)
Assertion
Ref Expression
co02 (𝐴 ∘ ∅) = ∅

Proof of Theorem co02
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relco 6078 . 2 Rel (𝐴 ∘ ∅)
2 rel0 5645 . 2 Rel ∅
3 br0 5084 . . . . . 6 ¬ 𝑥𝑧
43intnanr 491 . . . . 5 ¬ (𝑥𝑧𝑧𝐴𝑦)
54nex 1802 . . . 4 ¬ ∃𝑧(𝑥𝑧𝑧𝐴𝑦)
6 vex 3413 . . . . 5 𝑥 ∈ V
7 vex 3413 . . . . 5 𝑦 ∈ V
86, 7opelco 5716 . . . 4 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅) ↔ ∃𝑧(𝑥𝑧𝑧𝐴𝑦))
95, 8mtbir 326 . . 3 ¬ ⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅)
10 noel 4232 . . 3 ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
119, 102false 379 . 2 (⟨𝑥, 𝑦⟩ ∈ (𝐴 ∘ ∅) ↔ ⟨𝑥, 𝑦⟩ ∈ ∅)
121, 2, 11eqrelriiv 5636 1 (𝐴 ∘ ∅) = ∅
 Colors of variables: wff setvar class Syntax hints:   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∅c0 4227  ⟨cop 4531   class class class wbr 5035   ∘ ccom 5531 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-br 5036  df-opab 5098  df-xp 5533  df-rel 5534  df-co 5536 This theorem is referenced by:  co01  6095  relexpsucld  14446  gsumwmhm  18081  frmdgsum  18098  frmdup1  18100  efginvrel2  18925  0frgp  18977  evl1fval  21052  utop2nei  22956  tngds  23355  tocycf  30914  tocyc01  30915  mrsub0  32998  dfpo2  33242  cononrel1  40695
 Copyright terms: Public domain W3C validator