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 = { x | ( ( x i^i ( dom x X. ran x ) ) o. ( x i^i ( dom x X. ran x ) ) ) _S ( x i^i ( dom x X. ran x ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctrs	|- Trs
1		vx	|- x
2	1	cv	|- x
3	2	cdm	|- dom x
4	2	crn	|- ran x
5	3 4	cxp	|- ( dom x X. ran x )
6	2 5	cin	|- ( x i^i ( dom x X. ran x ) )
7	6 6	ccom	|- ( ( x i^i ( dom x X. ran x ) ) o. ( x i^i ( dom x X. ran x ) ) )
8		cssr	|- _S
9	7 6 8	wbr	|- ( ( x i^i ( dom x X. ran x ) ) o. ( x i^i ( dom x X. ran x ) ) ) _S ( x i^i ( dom x X. ran x ) )
10	9 1	cab	|- { x | ( ( x i^i ( dom x X. ran x ) ) o. ( x i^i ( dom x X. ran x ) ) ) _S ( x i^i ( dom x X. ran x ) ) }
11	0 10	wceq	|- Trs = { x | ( ( x i^i ( dom x X. ran x ) ) o. ( x i^i ( dom x X. ran x ) ) ) _S ( x i^i ( dom x X. ran x ) ) }