Definition df-trs

Description: Define the class of all transitive sets (versus the transitive class defined in df-tr ). It is used only by df-trrels .

Note the similarity of the definitions of df-refs , df-syms and df-trs . (Contributed by Peter Mazsa, 17-Jul-2021)

	Ref	Expression
Assertion	df-trs	⊢ Trs = { 𝑥 ∣ ( ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ∘ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrs	⊢ Trs
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3	2	cdm	⊢ dom 𝑥
4	2	crn	⊢ ran 𝑥
5	3 4	cxp	⊢ ( dom 𝑥 × ran 𝑥 )
6	2 5	cin	⊢ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) )
7	6 6	ccom	⊢ ( ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ∘ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) )
8		cssr	⊢ S
9	7 6 8	wbr	⊢ ( ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ∘ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) )
10	9 1	cab	⊢ { 𝑥 ∣ ( ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ∘ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }
11	0 10	wceq	⊢ Trs = { 𝑥 ∣ ( ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ∘ ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) ) S ( 𝑥 ∩ ( dom 𝑥 × ran 𝑥 ) ) }