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

Theorem ertr 6549
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 6543 . . . . . . 7 (𝑅 Er 𝑋 → Rel 𝑅)
31, 2syl 14 . . . . . 6 (𝜑 → Rel 𝑅)
4 simpr 110 . . . . . 6 ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐵𝑅𝐶)
5 brrelex 4666 . . . . . 6 ((Rel 𝑅𝐵𝑅𝐶) → 𝐵 ∈ V)
63, 4, 5syl2an 289 . . . . 5 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → 𝐵 ∈ V)
7 simpr 110 . . . . 5 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → (𝐴𝑅𝐵𝐵𝑅𝐶))
8 breq2 4007 . . . . . . 7 (𝑥 = 𝐵 → (𝐴𝑅𝑥𝐴𝑅𝐵))
9 breq1 4006 . . . . . . 7 (𝑥 = 𝐵 → (𝑥𝑅𝐶𝐵𝑅𝐶))
108, 9anbi12d 473 . . . . . 6 (𝑥 = 𝐵 → ((𝐴𝑅𝑥𝑥𝑅𝐶) ↔ (𝐴𝑅𝐵𝐵𝑅𝐶)))
1110spcegv 2825 . . . . 5 (𝐵 ∈ V → ((𝐴𝑅𝐵𝐵𝑅𝐶) → ∃𝑥(𝐴𝑅𝑥𝑥𝑅𝐶)))
126, 7, 11sylc 62 . . . 4 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → ∃𝑥(𝐴𝑅𝑥𝑥𝑅𝐶))
13 simpl 109 . . . . . 6 ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐵)
14 brrelex 4666 . . . . . 6 ((Rel 𝑅𝐴𝑅𝐵) → 𝐴 ∈ V)
153, 13, 14syl2an 289 . . . . 5 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → 𝐴 ∈ V)
16 brrelex2 4667 . . . . . 6 ((Rel 𝑅𝐵𝑅𝐶) → 𝐶 ∈ V)
173, 4, 16syl2an 289 . . . . 5 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → 𝐶 ∈ V)
18 brcog 4794 . . . . 5 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴(𝑅𝑅)𝐶 ↔ ∃𝑥(𝐴𝑅𝑥𝑥𝑅𝐶)))
1915, 17, 18syl2anc 411 . . . 4 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → (𝐴(𝑅𝑅)𝐶 ↔ ∃𝑥(𝐴𝑅𝑥𝑥𝑅𝐶)))
2012, 19mpbird 167 . . 3 ((𝜑 ∧ (𝐴𝑅𝐵𝐵𝑅𝐶)) → 𝐴(𝑅𝑅)𝐶)
2120ex 115 . 2 (𝜑 → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴(𝑅𝑅)𝐶))
22 df-er 6534 . . . . . 6 (𝑅 Er 𝑋 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝑋 ∧ (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅))
2322simp3bi 1014 . . . . 5 (𝑅 Er 𝑋 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
241, 23syl 14 . . . 4 (𝜑 → (𝑅 ∪ (𝑅𝑅)) ⊆ 𝑅)
2524unssbd 3313 . . 3 (𝜑 → (𝑅𝑅) ⊆ 𝑅)
2625ssbrd 4046 . 2 (𝜑 → (𝐴(𝑅𝑅)𝐶𝐴𝑅𝐶))
2721, 26syld 45 1 (𝜑 → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wex 1492  wcel 2148  Vcvv 2737  cun 3127  wss 3129   class class class wbr 4003  ccnv 4625  dom cdm 4626  ccom 4630  Rel wrel 4631   Er wer 6531
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004  df-opab 4065  df-xp 4632  df-rel 4633  df-co 4635  df-er 6534
This theorem is referenced by:  ertrd  6550  erth  6578  iinerm  6606  entr  6783
  Copyright terms: Public domain W3C validator