trclfvcom

Description: The transitive closure of a relation commutes with the relation. (Contributed by RP, 18-Jul-2020)

		Ref	Expression
	Assertion	trclfvcom	$⊢ R \in V \to t+ (R) \circ R = R \circ t+ (R)$

Step	Hyp	Ref	Expression
1		elex	$⊢ R \in V \to R \in V$
2		relexpsucnnr	$⊢ (R \in V \land n \in ℕ) \to R ↑_{r} (n + 1) = (R ↑_{r} n) \circ R$
3		relexpsucnnl	$⊢ (R \in V \land n \in ℕ) \to R ↑_{r} (n + 1) = R \circ (R ↑_{r} n)$
4	2 3	eqtr3d	$⊢ (R \in V \land n \in ℕ) \to (R ↑_{r} n) \circ R = R \circ (R ↑_{r} n)$
5	4	iuneq2dv	$⊢ R \in V \to ⋃_{n \in ℕ} ((R ↑_{r} n) \circ R) = ⋃_{n \in ℕ} (R \circ (R ↑_{r} n))$
6		oveq1	$⊢ r = R \to r ↑_{r} n = R ↑_{r} n$
7	6	iuneq2d	$⊢ r = R \to ⋃_{n \in ℕ} (r ↑_{r} n) = ⋃_{n \in ℕ} (R ↑_{r} n)$
8		dftrcl3	$⊢ t+ = (r \in V ⟼ ⋃_{n \in ℕ} (r ↑_{r} n))$
9		nnex	$⊢ ℕ \in V$
10		ovex	$⊢ R ↑_{r} n \in V$
11	9 10	iunex	$⊢ ⋃_{n \in ℕ} (R ↑_{r} n) \in V$
12	7 8 11	fvmpt	$⊢ R \in V \to t+ (R) = ⋃_{n \in ℕ} (R ↑_{r} n)$
13	12	coeq1d	$⊢ R \in V \to t+ (R) \circ R = ⋃_{n \in ℕ} (R ↑_{r} n) \circ R$
14		coiun1	$⊢ ⋃_{n \in ℕ} (R ↑_{r} n) \circ R = ⋃_{n \in ℕ} ((R ↑_{r} n) \circ R)$
15	13 14	eqtrdi	$⊢ R \in V \to t+ (R) \circ R = ⋃_{n \in ℕ} ((R ↑_{r} n) \circ R)$
16	12	coeq2d	$⊢ R \in V \to R \circ t+ (R) = R \circ ⋃_{n \in ℕ} (R ↑_{r} n)$
17		coiun	$⊢ R \circ ⋃_{n \in ℕ} (R ↑_{r} n) = ⋃_{n \in ℕ} (R \circ (R ↑_{r} n))$
18	16 17	eqtrdi	$⊢ R \in V \to R \circ t+ (R) = ⋃_{n \in ℕ} (R \circ (R ↑_{r} n))$
19	5 15 18	3eqtr4d	$⊢ R \in V \to t+ (R) \circ R = R \circ t+ (R)$
20	1 19	syl	$⊢ R \in V \to t+ (R) \circ R = R \circ t+ (R)$

Metamath Proof Explorer