Definition df-trans 5900

Description: Define the set of all transitive relationships over a base set. (Contributed by SF, 19-Feb-2015.)

Assertion

Ref	Expression
df-trans	|- Trans = {<.r, a>. | A.x e. a A.y e. a A.z e. a ((xry /\ yrz) -> xrz)}

Distinct variable group:   r,a,x,y,z

Detailed syntax breakdown of Definition df-trans

Step	Hyp	Ref	Expression
1		ctrans 5889	. 2 class Trans
2		vx	. . . . . . . . . 10 setvar x
3	2	cv 1641	. . . . . . . . 9 class x
4		vy	. . . . . . . . . 10 setvar y
5	4	cv 1641	. . . . . . . . 9 class y
6		vr	. . . . . . . . . 10 setvar r
7	6	cv 1641	. . . . . . . . 9 class r
8	3, 5, 7	wbr 4640	. . . . . . . 8 wff xry
9		vz	. . . . . . . . . 10 setvar z
10	9	cv 1641	. . . . . . . . 9 class z
11	5, 10, 7	wbr 4640	. . . . . . . 8 wff yrz
12	8, 11	wa 358	. . . . . . 7 wff (xry /\ yrz)
13	3, 10, 7	wbr 4640	. . . . . . 7 wff xrz
14	12, 13	wi 4	. . . . . 6 wff ((xry /\ yrz) -> xrz)
15		va	. . . . . . 7 setvar a
16	15	cv 1641	. . . . . 6 class a
17	14, 9, 16	wral 2615	. . . . 5 wff A.z e. a ((xry /\ yrz) -> xrz)
18	17, 4, 16	wral 2615	. . . 4 wff A.y e. a A.z e. a ((xry /\ yrz) -> xrz)
19	18, 2, 16	wral 2615	. . 3 wff A.x e. a A.y e. a A.z e. a ((xry /\ yrz) -> xrz)
20	19, 6, 15	copab 4623	. 2 class {<.r, a>. | A.x e. a A.y e. a A.z e. a ((xry /\ yrz) -> xrz)}
21	1, 20	wceq 1642	1 wff Trans = {<.r, a>. | A.x e. a A.y e. a A.z e. a ((xry /\ yrz) -> xrz)}

This definition is referenced by:  transex  5911  trd  5922  trrd  5926