trclfvdecomr

Description: The transitive closure of a relation may be decomposed into a union of the relation and the composition of the relation with its transitive closure. (Contributed by RP, 18-Jul-2020)

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

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ R \in V \to R \in V$
2		oveq1	$⊢ r = R \to r ↑_{r} n = R ↑_{r} n$
3	2	iuneq2d	$⊢ r = R \to ⋃_{n \in ℕ} (r ↑_{r} n) = ⋃_{n \in ℕ} (R ↑_{r} n)$
4		dftrcl3	$⊢ t+ = (r \in V ⟼ ⋃_{n \in ℕ} (r ↑_{r} n))$
5		nnex	$⊢ ℕ \in V$
6		ovex	$⊢ R ↑_{r} n \in V$
7	5 6	iunex	$⊢ ⋃_{n \in ℕ} (R ↑_{r} n) \in V$
8	3 4 7	fvmpt	$⊢ R \in V \to t+ (R) = ⋃_{n \in ℕ} (R ↑_{r} n)$
9	1 8	syl	$⊢ R \in V \to t+ (R) = ⋃_{n \in ℕ} (R ↑_{r} n)$
10		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
11		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
12		uzsplit	$⊢ 2 \in ℤ_{\geq 1} \to ℤ_{\geq 1} = (1 \dots 2 - 1) \cup ℤ_{\geq 2}$
13	11 12	ax-mp	$⊢ ℤ_{\geq 1} = (1 \dots 2 - 1) \cup ℤ_{\geq 2}$
14		2m1e1	$⊢ 2 - 1 = 1$
15	14	oveq2i	$⊢ (1 \dots 2 - 1) = (1 \dots 1)$
16		1z	$⊢ 1 \in ℤ$
17		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
18	16 17	ax-mp	$⊢ (1 \dots 1) = \{1\}$
19	15 18	eqtri	$⊢ (1 \dots 2 - 1) = \{1\}$
20	19	uneq1i	$⊢ (1 \dots 2 - 1) \cup ℤ_{\geq 2} = \{1\} \cup ℤ_{\geq 2}$
21	10 13 20	3eqtri	$⊢ ℕ = \{1\} \cup ℤ_{\geq 2}$
22		iuneq1	$⊢ ℕ = \{1\} \cup ℤ_{\geq 2} \to ⋃_{n \in ℕ} (R ↑_{r} n) = ⋃_{n \in \{1\} \cup ℤ_{\geq 2}} (R ↑_{r} n)$
23	21 22	ax-mp	$⊢ ⋃_{n \in ℕ} (R ↑_{r} n) = ⋃_{n \in \{1\} \cup ℤ_{\geq 2}} (R ↑_{r} n)$
24		iunxun	$⊢ ⋃_{n \in \{1\} \cup ℤ_{\geq 2}} (R ↑_{r} n) = ⋃_{n \in \{1\}} (R ↑_{r} n) \cup ⋃_{n \in ℤ_{\geq 2}} (R ↑_{r} n)$
25		1ex	$⊢ 1 \in V$
26		oveq2	$⊢ n = 1 \to R ↑_{r} n = R ↑_{r} 1$
27	25 26	iunxsn	$⊢ ⋃_{n \in \{1\}} (R ↑_{r} n) = R ↑_{r} 1$
28	27	uneq1i	$⊢ ⋃_{n \in \{1\}} (R ↑_{r} n) \cup ⋃_{n \in ℤ_{\geq 2}} (R ↑_{r} n) = (R ↑_{r} 1) \cup ⋃_{n \in ℤ_{\geq 2}} (R ↑_{r} n)$
29	23 24 28	3eqtri	$⊢ ⋃_{n \in ℕ} (R ↑_{r} n) = (R ↑_{r} 1) \cup ⋃_{n \in ℤ_{\geq 2}} (R ↑_{r} n)$
30		relexp1g	$⊢ R \in V \to R ↑_{r} 1 = R$
31		oveq1	$⊢ r = R \to r ↑_{r} m = R ↑_{r} m$
32	31	iuneq2d	$⊢ r = R \to ⋃_{m \in ℕ} (r ↑_{r} m) = ⋃_{m \in ℕ} (R ↑_{r} m)$
33		dftrcl3	$⊢ t+ = (r \in V ⟼ ⋃_{m \in ℕ} (r ↑_{r} m))$
34		ovex	$⊢ R ↑_{r} m \in V$
35	5 34	iunex	$⊢ ⋃_{m \in ℕ} (R ↑_{r} m) \in V$
36	32 33 35	fvmpt	$⊢ R \in V \to t+ (R) = ⋃_{m \in ℕ} (R ↑_{r} m)$
37	1 36	syl	$⊢ R \in V \to t+ (R) = ⋃_{m \in ℕ} (R ↑_{r} m)$
38	37	coeq1d	$⊢ R \in V \to t+ (R) \circ R = ⋃_{m \in ℕ} (R ↑_{r} m) \circ R$
39		coiun1	$⊢ ⋃_{m \in ℕ} (R ↑_{r} m) \circ R = ⋃_{m \in ℕ} ((R ↑_{r} m) \circ R)$
40		uz2m1nn	$⊢ n \in ℤ_{\geq 2} \to n - 1 \in ℕ$
41	40	adantl	$⊢ (R \in V \land n \in ℤ_{\geq 2}) \to n - 1 \in ℕ$
42		eluzp1p1	$⊢ m \in ℤ_{\geq 1} \to m + 1 \in ℤ_{\geq (1 + 1)}$
43	42 10	eleq2s	$⊢ m \in ℕ \to m + 1 \in ℤ_{\geq (1 + 1)}$
44		1p1e2	$⊢ 1 + 1 = 2$
45	44	fveq2i	$⊢ ℤ_{\geq (1 + 1)} = ℤ_{\geq 2}$
46	43 45	eleqtrdi	$⊢ m \in ℕ \to m + 1 \in ℤ_{\geq 2}$
47	46	adantl	$⊢ (R \in V \land m \in ℕ) \to m + 1 \in ℤ_{\geq 2}$
48		oveq2	$⊢ m = n - 1 \to R ↑_{r} m = R ↑_{r} (n - 1)$
49	48	coeq1d	$⊢ m = n - 1 \to (R ↑_{r} m) \circ R = (R ↑_{r} (n - 1)) \circ R$
50	49	3ad2ant3	$⊢ (R \in V \land n \in ℤ_{\geq 2} \land m = n - 1) \to (R ↑_{r} m) \circ R = (R ↑_{r} (n - 1)) \circ R$
51		oveq2	$⊢ n = m + 1 \to R ↑_{r} n = R ↑_{r} (m + 1)$
52	51	3ad2ant3	$⊢ (R \in V \land m \in ℕ \land n = m + 1) \to R ↑_{r} n = R ↑_{r} (m + 1)$
53		relexpsucnnr	$⊢ (R \in V \land m \in ℕ) \to R ↑_{r} (m + 1) = (R ↑_{r} m) \circ R$
54	53	eqcomd	$⊢ (R \in V \land m \in ℕ) \to (R ↑_{r} m) \circ R = R ↑_{r} (m + 1)$
55		relexpsucnnr	$⊢ (R \in V \land n - 1 \in ℕ) \to R ↑_{r} (n - 1 + 1) = (R ↑_{r} (n - 1)) \circ R$
56	40 55	sylan2	$⊢ (R \in V \land n \in ℤ_{\geq 2}) \to R ↑_{r} (n - 1 + 1) = (R ↑_{r} (n - 1)) \circ R$
57		eluzelcn	$⊢ n \in ℤ_{\geq 2} \to n \in ℂ$
58		npcan1	$⊢ n \in ℂ \to n - 1 + 1 = n$
59		oveq2	$⊢ n - 1 + 1 = n \to R ↑_{r} (n - 1 + 1) = R ↑_{r} n$
60	57 58 59	3syl	$⊢ n \in ℤ_{\geq 2} \to R ↑_{r} (n - 1 + 1) = R ↑_{r} n$
61	60	eqeq1d	$⊢ n \in ℤ_{\geq 2} \to (R ↑_{r} (n - 1 + 1) = (R ↑_{r} (n - 1)) \circ R \leftrightarrow R ↑_{r} n = (R ↑_{r} (n - 1)) \circ R)$
62	61	adantl	$⊢ (R \in V \land n \in ℤ_{\geq 2}) \to (R ↑_{r} (n - 1 + 1) = (R ↑_{r} (n - 1)) \circ R \leftrightarrow R ↑_{r} n = (R ↑_{r} (n - 1)) \circ R)$
63	56 62	mpbid	$⊢ (R \in V \land n \in ℤ_{\geq 2}) \to R ↑_{r} n = (R ↑_{r} (n - 1)) \circ R$
64	41 47 50 52 54 63	cbviuneq12dv	$⊢ R \in V \to ⋃_{m \in ℕ} ((R ↑_{r} m) \circ R) = ⋃_{n \in ℤ_{\geq 2}} (R ↑_{r} n)$
65	39 64	eqtrid	$⊢ R \in V \to ⋃_{m \in ℕ} (R ↑_{r} m) \circ R = ⋃_{n \in ℤ_{\geq 2}} (R ↑_{r} n)$
66	38 65	eqtrd	$⊢ R \in V \to t+ (R) \circ R = ⋃_{n \in ℤ_{\geq 2}} (R ↑_{r} n)$
67	66	eqcomd	$⊢ R \in V \to ⋃_{n \in ℤ_{\geq 2}} (R ↑_{r} n) = t+ (R) \circ R$
68	30 67	uneq12d	$⊢ R \in V \to (R ↑_{r} 1) \cup ⋃_{n \in ℤ_{\geq 2}} (R ↑_{r} n) = R \cup (t+ (R) \circ R)$
69	29 68	eqtrid	$⊢ R \in V \to ⋃_{n \in ℕ} (R ↑_{r} n) = R \cup (t+ (R) \circ R)$
70	9 69	eqtrd	$⊢ R \in V \to t+ (R) = R \cup (t+ (R) \circ R)$

Metamath Proof Explorer

Theorem trclfvdecomr

Proof