df-rtrcl

Description: Reflexive-transitive closure of a relation. This is the smallest superset which is reflexive property over all elements of its domain and range and has the transitive property. (Contributed by FL, 27-Jun-2011)

		Ref	Expression
	Assertion	df-rtrcl	$⊢ t* = (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crtcl	$class t*$
1		vx	$setvar x$
2		cvv	$class V$
3		vz	$setvar z$
4		cid	$class I$
5	1	cv	$setvar x$
6	5	cdm	$class dom x$
7	5	crn	$class ran x$
8	6 7	cun	$class (dom x \cup ran x)$
9	4 8	cres	$class ({I ↾}_{(dom x \cup ran x)})$
10	3	cv	$setvar z$
11	9 10	wss	$wff {I ↾}_{(dom x \cup ran x)} \subseteq z$
12	5 10	wss	$wff x \subseteq z$
13	10 10	ccom	$class (z \circ z)$
14	13 10	wss	$wff z \circ z \subseteq z$
15	11 12 14	w3a	$wff ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)$
16	15 3	cab	$class \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}$
17	16	cint	$class ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\}$
18	1 2 17	cmpt	$class (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\})$
19	0 18	wceq	$wff t* = (x \in V ⟼ ⋂ \{z \| ({I ↾}_{(dom x \cup ran x)} \subseteq z \land x \subseteq z \land z \circ z \subseteq z)\})$

Metamath Proof Explorer

Definition df-rtrcl

Detailed syntax breakdown