dfrcl4

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

		Ref	Expression
	Assertion	dfrcl4	$⊢ r* = (r \in V ⟼ ⋃_{n \in \{0, 1\}} (r ↑_{r} n))$

Step	Hyp	Ref	Expression
1		dfrcl3	$⊢ r* = (r \in V ⟼ (r ↑_{r} 0) \cup (r ↑_{r} 1))$
2		df-pr	$⊢ \{0, 1\} = \{0\} \cup \{1\}$
3		iuneq1	$⊢ \{0, 1\} = \{0\} \cup \{1\} \to ⋃_{n \in \{0, 1\}} (r ↑_{r} n) = ⋃_{n \in \{0\} \cup \{1\}} (r ↑_{r} n)$
4	2 3	ax-mp	$⊢ ⋃_{n \in \{0, 1\}} (r ↑_{r} n) = ⋃_{n \in \{0\} \cup \{1\}} (r ↑_{r} n)$
5		iunxun	$⊢ ⋃_{n \in \{0\} \cup \{1\}} (r ↑_{r} n) = ⋃_{n \in \{0\}} (r ↑_{r} n) \cup ⋃_{n \in \{1\}} (r ↑_{r} n)$
6		c0ex	$⊢ 0 \in V$
7		oveq2	$⊢ n = 0 \to r ↑_{r} n = r ↑_{r} 0$
8	6 7	iunxsn	$⊢ ⋃_{n \in \{0\}} (r ↑_{r} n) = r ↑_{r} 0$
9		1ex	$⊢ 1 \in V$
10		oveq2	$⊢ n = 1 \to r ↑_{r} n = r ↑_{r} 1$
11	9 10	iunxsn	$⊢ ⋃_{n \in \{1\}} (r ↑_{r} n) = r ↑_{r} 1$
12	8 11	uneq12i	$⊢ ⋃_{n \in \{0\}} (r ↑_{r} n) \cup ⋃_{n \in \{1\}} (r ↑_{r} n) = (r ↑_{r} 0) \cup (r ↑_{r} 1)$
13	4 5 12	3eqtri	$⊢ ⋃_{n \in \{0, 1\}} (r ↑_{r} n) = (r ↑_{r} 0) \cup (r ↑_{r} 1)$
14	13	mpteq2i	$⊢ (r \in V ⟼ ⋃_{n \in \{0, 1\}} (r ↑_{r} n)) = (r \in V ⟼ (r ↑_{r} 0) \cup (r ↑_{r} 1))$
15	1 14	eqtr4i	$⊢ r* = (r \in V ⟼ ⋃_{n \in \{0, 1\}} (r ↑_{r} n))$

Metamath Proof Explorer