dfrtrcl4

Description: Reflexive-transitive closure of a relation, expressed as the union of the zeroth power and the transitive closure. (Contributed by RP, 5-Jun-2020)

		Ref	Expression
	Assertion	dfrtrcl4	$⊢ t* = (r \in V ⟼ (r ↑_{r} 0) \cup t+ (r))$

Proof

Step	Hyp	Ref	Expression
1		dfrtrcl3	$⊢ t* = (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n))$
2		df-n0	$⊢ ℕ_{0} = ℕ \cup \{0\}$
3	2	equncomi	$⊢ ℕ_{0} = \{0\} \cup ℕ$
4		iuneq1	$⊢ ℕ_{0} = \{0\} \cup ℕ \to ⋃_{n \in ℕ_{0}} (r ↑_{r} n) = ⋃_{n \in \{0\} \cup ℕ} (r ↑_{r} n)$
5	3 4	ax-mp	$⊢ ⋃_{n \in ℕ_{0}} (r ↑_{r} n) = ⋃_{n \in \{0\} \cup ℕ} (r ↑_{r} n)$
6		iunxun	$⊢ ⋃_{n \in \{0\} \cup ℕ} (r ↑_{r} n) = ⋃_{n \in \{0\}} (r ↑_{r} n) \cup ⋃_{n \in ℕ} (r ↑_{r} n)$
7	5 6	eqtri	$⊢ ⋃_{n \in ℕ_{0}} (r ↑_{r} n) = ⋃_{n \in \{0\}} (r ↑_{r} n) \cup ⋃_{n \in ℕ} (r ↑_{r} n)$
8		c0ex	$⊢ 0 \in V$
9		oveq2	$⊢ n = 0 \to r ↑_{r} n = r ↑_{r} 0$
10	8 9	iunxsn	$⊢ ⋃_{n \in \{0\}} (r ↑_{r} n) = r ↑_{r} 0$
11	10	a1i	$⊢ r \in V \to ⋃_{n \in \{0\}} (r ↑_{r} n) = r ↑_{r} 0$
12		oveq1	$⊢ x = r \to x ↑_{r} n = r ↑_{r} n$
13	12	iuneq2d	$⊢ x = r \to ⋃_{n \in ℕ} (x ↑_{r} n) = ⋃_{n \in ℕ} (r ↑_{r} n)$
14		dftrcl3	$⊢ t+ = (x \in V ⟼ ⋃_{n \in ℕ} (x ↑_{r} n))$
15		nnex	$⊢ ℕ \in V$
16		ovex	$⊢ r ↑_{r} n \in V$
17	15 16	iunex	$⊢ ⋃_{n \in ℕ} (r ↑_{r} n) \in V$
18	13 14 17	fvmpt	$⊢ r \in V \to t+ (r) = ⋃_{n \in ℕ} (r ↑_{r} n)$
19	18	eqcomd	$⊢ r \in V \to ⋃_{n \in ℕ} (r ↑_{r} n) = t+ (r)$
20	11 19	uneq12d	$⊢ r \in V \to ⋃_{n \in \{0\}} (r ↑_{r} n) \cup ⋃_{n \in ℕ} (r ↑_{r} n) = (r ↑_{r} 0) \cup t+ (r)$
21	7 20	syl5eq	$⊢ r \in V \to ⋃_{n \in ℕ_{0}} (r ↑_{r} n) = (r ↑_{r} 0) \cup t+ (r)$
22	21	mpteq2ia	$⊢ (r \in V ⟼ ⋃_{n \in ℕ_{0}} (r ↑_{r} n)) = (r \in V ⟼ (r ↑_{r} 0) \cup t+ (r))$
23	1 22	eqtri	$⊢ t* = (r \in V ⟼ (r ↑_{r} 0) \cup t+ (r))$

Metamath Proof Explorer

Theorem dfrtrcl4

Proof