Theorem dftrrels2 39559

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 5660 (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑢(𝑥𝐵𝑢 ∧ 𝑢𝐴𝑦)} 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 39401 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

Step	Hyp	Ref	Expression
1		df-trrels 39557	. 2 ⊢ TrRels = ( Trs ∩ Rels )
2		df-trs 39556	. 2 ⊢ Trs = {𝑟 ∣ ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟))}
3		inex1g 5279	. . . . 5 ⊢ (𝑟 ∈ V → (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∈ V)
4	3	elv 3456	. . . 4 ⊢ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∈ V
5		brssr 39481	. . . 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 39345	. . . . . . 7 ⊢ (𝑟 ∈ V → (𝑟 ∈ Rels ↔ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟))
8	7	elv 3456	. . . . . 6 ⊢ (𝑟 ∈ Rels ↔ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟)
9	8	biimpi 219	. . . . 5 ⊢ (𝑟 ∈ Rels → (𝑟 ∩ (dom 𝑟 × ran 𝑟)) = 𝑟)
10	9, 9	coeq12d 5842	. . . 4 ⊢ (𝑟 ∈ Rels → ((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) = (𝑟 ∘ 𝑟))
11	10, 9	sseq12d 3964	. . 3 ⊢ (𝑟 ∈ Rels → (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) ⊆ (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ (𝑟 ∘ 𝑟) ⊆ 𝑟))
12	6, 11	bitrid 286	. 2 ⊢ (𝑟 ∈ Rels → (((𝑟 ∩ (dom 𝑟 × ran 𝑟)) ∘ (𝑟 ∩ (dom 𝑟 × ran 𝑟))) S (𝑟 ∩ (dom 𝑟 × ran 𝑟)) ↔ (𝑟 ∘ 𝑟) ⊆ 𝑟))
13	1, 2, 12	abeqinbi 39155	1 ⊢ TrRels = {𝑟 ∈ Rels ∣ (𝑟 ∘ 𝑟) ⊆ 𝑟}

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {crab 3413  Vcvv 3451   ∩ cin 3898   ⊆ wss 3899   class class class wbr 5103   × cxp 5649  dom cdm 5651  ran crn 5652   ∘ ccom 5655   Rels crels 39085   S cssr 39086   Trs ctrs 39096   TrRels ctrrels 39097

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-rels 39340  df-ssr 39478  df-trs 39556  df-trrels 39557

This theorem is used by:  dftrrels3  39560  eltrrels2  39563  dfeqvrels2  39572