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⟩ ∣ ∀x ∈ a ∀y ∈ a ∀z ∈ 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 ∀z ∈ a ((xry ∧ yrz) → xrz)
18	17, 4, 16	wral 2615	. . . 4 wff ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)
19	18, 2, 16	wral 2615	. . 3 wff ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)
20	19, 6, 15	copab 4623	. 2 class {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)}
21	1, 20	wceq 1642	1 wff Trans = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ∀z ∈ a ((xry ∧ yrz) → xrz)}

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