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

Theorem ertr 8338
Description: An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
Hypothesis
Ref Expression
ersymb.1 (𝜑𝑅 Er 𝑋)
Assertion
Ref Expression
ertr (𝜑 → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))

Proof of Theorem ertr
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ersymb.1 . . . . . . 7 (𝜑𝑅 Er 𝑋)
2 errel 8332 . . . . . . 7 (𝑅 Er 𝑋 → Rel 𝑅)
31, 2syl 17 . . . . . 6 (𝜑 → Rel 𝑅)
4 simpr 488 . . . . . 6 ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐵𝑅𝐶)
5 brrelex1 5577 . . . . . 6 ((Rel 𝑅𝐵𝑅𝐶) → 𝐵 ∈ V)
63, 4, 5syl2an 599 . . . . 5 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → 𝐵 ∈ V)
7 simpr 488 . . . . 5 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → (𝐴𝑅𝐵𝐵𝑅𝐶))
8 breq2 5035 . . . . . 6 (𝑥 = 𝐵 → (𝐴𝑅𝑥𝐴𝑅𝐵))
9 breq1 5034 . . . . . 6 (𝑥 = 𝐵 → (𝑥𝑅𝐶𝐵𝑅𝐶))
108, 9anbi12d 634 . . . . 5 (𝑥 = 𝐵 → ((𝐴𝑅𝑥𝑥𝑅𝐶) ↔ (𝐴𝑅𝐵𝐵𝑅𝐶)))
116, 7, 10spcedv 3503 . . . 4 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → ∃𝑥(𝐴𝑅𝑥𝑥𝑅𝐶))
12 simpl 486 . . . . . 6 ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐵)
13 brrelex1 5577 . . . . . 6 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ V)
143, 12, 13syl2an 599 . . . . 5 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → 𝐴 ∈ V)
15 brrelex2 5578 . . . . . 6 ((Rel 𝑅𝐵𝑅𝐶) → 𝐶 ∈ V)
163, 4, 15syl2an 599 . . . . 5 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → 𝐶 ∈ V)
17 brcog 5710 . . . . 5 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴(𝑅𝑅)𝐶 ↔ ∃𝑥(𝐴𝑅𝑥𝑥𝑅𝐶)))
1814, 16, 17syl2anc 587 . . . 4 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → (𝐴(𝑅𝑅)𝐶 ↔ ∃𝑥(𝐴𝑅𝑥𝑥𝑅𝐶)))
1911, 18mpbird 260 . . 3 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → 𝐴(𝑅𝑅)𝐶)
2019ex 416 . 2 (𝜑 → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴(𝑅𝑅)𝐶))
21 df-er 8323 . . . . . 6 (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
2221simp3bi 1148 . . . . 5 (𝑅 Er 𝑋 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
231, 22syl 17 . . . 4 (𝜑 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
2423unssbd 4079 . . 3 (𝜑 → (𝑅𝑅) ⊆ 𝑅)
2524ssbrd 5074 . 2 (𝜑 → (𝐴(𝑅𝑅)𝐶𝐴𝑅𝐶))
2620, 25syld 47 1 (𝜑 → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542  wex 1786  wcel 2114  Vcvv 3399  cun 3842  wss 3844   class class class wbr 5031  ccnv 5525  dom cdm 5526  ccom 5530  Rel wrel 5531   Er wer 8320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711  ax-sep 5168  ax-nul 5175  ax-pr 5297
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-ral 3059  df-rex 3060  df-v 3401  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-br 5032  df-opab 5094  df-xp 5532  df-rel 5533  df-co 5535  df-er 8323
This theorem is referenced by:  ertrd  8339  erth  8372  iiner  8403  entr  8610  efginvrel2  18974  efgsrel  18981
  Copyright terms: Public domain W3C validator