Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dftrrels2 Structured version   Visualization version   GIF version

Theorem dftrrels2 38576
Description: Alternate definition of the class of transitive relations.

I'd prefer to define the class of transitive relations by using the definition of composition by [Suppes] p. 63. df-coSUP (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐴𝑢𝑢𝐵𝑦)} as opposed to the present definition of composition df-co 5694 (𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐵𝑢𝑢𝐴𝑦)} because the Suppes definition keeps the order of 𝐴, 𝐵, 𝐶, 𝑅, 𝑆, 𝑇 by default in trsinxpSUP (((𝑅 ∩ (𝐴 × 𝐵)) ∘ (𝑆 ∩ (𝐵 × 𝐶))) ⊆ (𝑇 ∩ (𝐴 × 𝐶)) ↔ ∀𝑥𝐴𝑦𝐵 𝑧𝐶((𝑥𝑅𝑦𝑦𝑆𝑧) → 𝑥𝑇𝑧)) while the present definition of composition disarranges them: trsinxp (((𝑆 ∩ (𝐵 × 𝐶)) ∘ (𝑅 ∩ (𝐴 × 𝐵))) ⊆ (𝑇 ∩ (𝐴 × 𝐶 )) ↔ ∀𝑥𝐴𝑦𝐵𝑧𝐶((𝑥𝑅𝑦𝑦𝑆𝑧) → 𝑥𝑇𝑧) ). This is not mission critical to me, the implication of the Suppes definition is just more aesthetic, at least in the above case.

If we swap to the Suppes definition of class composition, I would define the present class of all transitive sets as df-trsSUP and I would consider to switch the definition of the class of cosets by 𝑅 from the present df-coss 38412 to a df-cossSUP. But perhaps there is a mathematical reason to keep the present definition of composition. (Contributed by Peter Mazsa, 21-Jul-2021.)

Assertion
Ref Expression
dftrrels2 TrRels = {𝑟 ∈ Rels ∣ (𝑟𝑟) ⊆ 𝑟}

Proof of Theorem dftrrels2
StepHypRef Expression
1 df-trrels 38574 . 2 TrRels = ( Trs ∩ Rels )
2 df-trs 38573 . 2 Trs = {𝑟 ∣ ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟))}
3 inex1g 5319 . . . . 5 (𝑟 ∈ V → (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∈ V)
43elv 3485 . . . 4 (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∈ V
5 brssr 38502 . . . 4 ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∈ V → (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) ⊆ (𝑟 ∩ (dom 𝑟 × ran 𝑟))))
64, 5ax-mp 5 . . 3 (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) ⊆ (𝑟 ∩ (dom 𝑟 × ran 𝑟)))
7 elrels6 38491 . . . . . . 7 (𝑟 ∈ V → (𝑟 ∈ Rels ↔ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟))
87elv 3485 . . . . . 6 (𝑟 ∈ Rels ↔ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟)
98biimpi 216 . . . . 5 (𝑟 ∈ Rels → (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟)
109, 9coeq12d 5875 . . . 4 (𝑟 ∈ Rels → ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) = (𝑟𝑟))
1110, 9sseq12d 4017 . . 3 (𝑟 ∈ Rels → (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) ⊆ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ (𝑟𝑟) ⊆ 𝑟))
126, 11bitrid 283 . 2 (𝑟 ∈ Rels → (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ (𝑟𝑟) ⊆ 𝑟))
131, 2, 12abeqinbi 38254 1 TrRels = {𝑟 ∈ Rels ∣ (𝑟𝑟) ⊆ 𝑟}
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  wcel 2108  {crab 3436  Vcvv 3480  cin 3950  wss 3951   class class class wbr 5143   × cxp 5683  dom cdm 5685  ran crn 5686  ccom 5689   Rels crels 38184   S cssr 38185   Trs ctrs 38195   TrRels ctrrels 38196
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-rels 38486  df-ssr 38499  df-trs 38573  df-trrels 38574
This theorem is referenced by:  dftrrels3  38577  eltrrels2  38580  dfeqvrels2  38589
  Copyright terms: Public domain W3C validator