dfrcl3

Description: Reflexive closure of a relation as union of powers of the relation. (Contributed by RP, 6-Jun-2020)

		Ref	Expression
	Assertion	dfrcl3	$⊢ r* = (x \in V ⟼ (x ↑_{r} 0) \cup (x ↑_{r} 1))$

Step	Hyp	Ref	Expression
1		dfrcl2	$⊢ r* = (x \in V ⟼ ({I ↾}_{(dom x \cup ran x)}) \cup x)$
2		relexp0g	$⊢ x \in V \to x ↑_{r} 0 = {I ↾}_{(dom x \cup ran x)}$
3		relexp1g	$⊢ x \in V \to x ↑_{r} 1 = x$
4	2 3	uneq12d	$⊢ x \in V \to (x ↑_{r} 0) \cup (x ↑_{r} 1) = ({I ↾}_{(dom x \cup ran x)}) \cup x$
5	4	mpteq2ia	$⊢ (x \in V ⟼ (x ↑_{r} 0) \cup (x ↑_{r} 1)) = (x \in V ⟼ ({I ↾}_{(dom x \cup ran x)}) \cup x)$
6	1 5	eqtr4i	$⊢ r* = (x \in V ⟼ (x ↑_{r} 0) \cup (x ↑_{r} 1))$

Metamath Proof Explorer