ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ertr Structured version   Unicode version

Theorem ertr 6057
Description: An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
Hypothesis
Ref Expression
ersymb.1  R  Er  X
Assertion
Ref Expression
ertr  R  R C  R C

Proof of Theorem ertr
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ersymb.1 . . . . . . 7  R  Er  X
2 errel 6051 . . . . . . 7  R  Er  X  Rel  R
31, 2syl 14 . . . . . 6  Rel  R
4 simpr 103 . . . . . 6  R  R C  R C
5 brrelex 4325 . . . . . 6  Rel  R  R C  _V
63, 4, 5syl2an 273 . . . . 5  R  R C  _V
7 simpr 103 . . . . 5  R  R C  R  R C
8 breq2 3759 . . . . . . 7  R  R
9 breq1 3758 . . . . . . 7  R C  R C
108, 9anbi12d 442 . . . . . 6  R  R C  R  R C
1110spcegv 2635 . . . . 5  _V  R  R C  R  R C
126, 7, 11sylc 56 . . . 4  R  R C  R  R C
13 simpl 102 . . . . . 6  R  R C  R
14 brrelex 4325 . . . . . 6  Rel  R  R  _V
153, 13, 14syl2an 273 . . . . 5  R  R C  _V
16 brrelex2 4326 . . . . . 6  Rel  R  R C  C  _V
173, 4, 16syl2an 273 . . . . 5  R  R C  C  _V
18 brcog 4445 . . . . 5  _V  C  _V  R  o.  R C  R  R C
1915, 17, 18syl2anc 391 . . . 4  R  R C  R  o.  R C  R  R C
2012, 19mpbird 156 . . 3  R  R C  R  o.  R C
2120ex 108 . 2  R  R C  R  o.  R C
22 df-er 6042 . . . . . 6  R  Er  X  Rel 
R  dom  R  X  `' R  u.  R  o.  R 
C_  R
2322simp3bi 920 . . . . 5  R  Er  X  `' R  u.  R  o.  R  C_  R
241, 23syl 14 . . . 4  `' R  u.  R  o.  R  C_  R
2524unssbd 3115 . . 3  R  o.  R  C_  R
2625ssbrd 3796 . 2  R  o.  R C  R C
2721, 26syld 40 1  R  R C  R C
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98   wceq 1242  wex 1378   wcel 1390   _Vcvv 2551    u. cun 2909    C_ wss 2911   class class class wbr 3755   `'ccnv 4287   dom cdm 4288    o. ccom 4292   Rel wrel 4293    Er wer 6039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-xp 4294  df-rel 4295  df-co 4297  df-er 6042
This theorem is referenced by:  ertrd  6058  erth  6086  iinerm  6114  entr  6200
  Copyright terms: Public domain W3C validator