![]() |
Mathbox for Peter Mazsa |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > dftrrels2 | Structured version Visualization version GIF version |
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 5681 (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} 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 37939 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.) |
Ref | Expression |
---|---|
dftrrels2 | ⊢ TrRels = {𝑟 ∈ Rels ∣ (𝑟 ∘ 𝑟) ⊆ 𝑟} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-trrels 38101 | . 2 ⊢ TrRels = ( Trs ∩ Rels ) | |
2 | df-trs 38100 | . 2 ⊢ Trs = {𝑟 ∣ ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟))} | |
3 | inex1g 5314 | . . . . 5 ⊢ (𝑟 ∈ V → (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∈ V) | |
4 | 3 | elv 3469 | . . . 4 ⊢ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∈ V |
5 | brssr 38029 | . . . 4 ⊢ ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∈ V → (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) ⊆ (𝑟 ∩ (dom 𝑟 × ran 𝑟)))) | |
6 | 4, 5 | ax-mp 5 | . . 3 ⊢ (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) ⊆ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) |
7 | elrels6 38018 | . . . . . . 7 ⊢ (𝑟 ∈ V → (𝑟 ∈ Rels ↔ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟)) | |
8 | 7 | elv 3469 | . . . . . 6 ⊢ (𝑟 ∈ Rels ↔ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟) |
9 | 8 | biimpi 215 | . . . . 5 ⊢ (𝑟 ∈ Rels → (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟) |
10 | 9, 9 | coeq12d 5861 | . . . 4 ⊢ (𝑟 ∈ Rels → ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) = (𝑟 ∘ 𝑟)) |
11 | 10, 9 | sseq12d 4006 | . . 3 ⊢ (𝑟 ∈ Rels → (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) ⊆ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ (𝑟 ∘ 𝑟) ⊆ 𝑟)) |
12 | 6, 11 | bitrid 282 | . 2 ⊢ (𝑟 ∈ Rels → (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ (𝑟 ∘ 𝑟) ⊆ 𝑟)) |
13 | 1, 2, 12 | abeqinbi 37781 | 1 ⊢ TrRels = {𝑟 ∈ Rels ∣ (𝑟 ∘ 𝑟) ⊆ 𝑟} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1533 ∈ wcel 2098 {crab 3419 Vcvv 3463 ∩ cin 3938 ⊆ wss 3939 class class class wbr 5143 × cxp 5670 dom cdm 5672 ran crn 5673 ∘ ccom 5676 Rels crels 37707 S cssr 37708 Trs ctrs 37718 TrRels ctrrels 37719 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5294 ax-nul 5301 ax-pr 5423 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3465 df-dif 3942 df-un 3944 df-in 3946 df-ss 3956 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-br 5144 df-opab 5206 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-rels 38013 df-ssr 38026 df-trs 38100 df-trrels 38101 |
This theorem is referenced by: dftrrels3 38104 eltrrels2 38107 dfeqvrels2 38116 |
Copyright terms: Public domain | W3C validator |