HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  chjcomi Structured version   Visualization version   GIF version

Theorem chjcomi 29573
Description: Commutative law for join in C. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.)
Hypotheses
Ref Expression
ch0le.1 𝐴C
chjcl.2 𝐵C
Assertion
Ref Expression
chjcomi (𝐴 𝐵) = (𝐵 𝐴)

Proof of Theorem chjcomi
StepHypRef Expression
1 ch0le.1 . . 3 𝐴C
21chshii 29332 . 2 𝐴S
3 chjcl.2 . . 3 𝐵C
43chshii 29332 . 2 𝐵S
52, 4shjcomi 29476 1 (𝐴 𝐵) = (𝐵 𝐴)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  wcel 2111  (class class class)co 7231   C cch 29034   chj 29038
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-sep 5206  ax-nul 5213  ax-pr 5336  ax-hilex 29104
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ral 3067  df-rex 3068  df-rab 3071  df-v 3422  df-sbc 3709  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4834  df-br 5068  df-opab 5130  df-id 5469  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-iota 6355  df-fun 6399  df-fv 6405  df-ov 7234  df-oprab 7235  df-mpo 7236  df-sh 29312  df-ch 29326  df-chj 29415
This theorem is referenced by:  chub2i  29575  chnlei  29590  chj12i  29627  lejdiri  29644  cmcm2i  29698  cmbr3i  29705  qlax2i  29733  osumcor2i  29749  3oalem5  29771  pjcji  29789  mayetes3i  29834  mdslj2i  30425  mdsl1i  30426  cvmdi  30429  mdslmd2i  30435  mdexchi  30440  cvexchi  30474  atabsi  30506  mdsymlem1  30508  mdsymlem6  30513  mdsymlem8  30515  sumdmdlem2  30524  dmdbr5ati  30527
  Copyright terms: Public domain W3C validator