![]() |
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 5686 (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} 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 37281 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 37443 | . 2 ⊢ TrRels = ( Trs ∩ Rels ) | |
2 | df-trs 37442 | . 2 ⊢ Trs = {𝑟 ∣ ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟))} | |
3 | inex1g 5320 | . . . . 5 ⊢ (𝑟 ∈ V → (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∈ V) | |
4 | 3 | elv 3481 | . . . 4 ⊢ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∈ V |
5 | brssr 37371 | . . . 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 37360 | . . . . . . 7 ⊢ (𝑟 ∈ V → (𝑟 ∈ Rels ↔ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟)) | |
8 | 7 | elv 3481 | . . . . . 6 ⊢ (𝑟 ∈ Rels ↔ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟) |
9 | 8 | biimpi 215 | . . . . 5 ⊢ (𝑟 ∈ Rels → (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟) |
10 | 9, 9 | coeq12d 5865 | . . . 4 ⊢ (𝑟 ∈ Rels → ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) = (𝑟 ∘ 𝑟)) |
11 | 10, 9 | sseq12d 4016 | . . 3 ⊢ (𝑟 ∈ Rels → (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) ⊆ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ (𝑟 ∘ 𝑟) ⊆ 𝑟)) |
12 | 6, 11 | bitrid 283 | . 2 ⊢ (𝑟 ∈ Rels → (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ (𝑟 ∘ 𝑟) ⊆ 𝑟)) |
13 | 1, 2, 12 | abeqinbi 37121 | 1 ⊢ TrRels = {𝑟 ∈ Rels ∣ (𝑟 ∘ 𝑟) ⊆ 𝑟} |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1542 ∈ wcel 2107 {crab 3433 Vcvv 3475 ∩ cin 3948 ⊆ wss 3949 class class class wbr 5149 × cxp 5675 dom cdm 5677 ran crn 5678 ∘ ccom 5681 Rels crels 37045 S cssr 37046 Trs ctrs 37056 TrRels ctrrels 37057 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-br 5150 df-opab 5212 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-rels 37355 df-ssr 37368 df-trs 37442 df-trrels 37443 |
This theorem is referenced by: dftrrels3 37446 eltrrels2 37449 dfeqvrels2 37458 |
Copyright terms: Public domain | W3C validator |