trclrelexplem

Description: The union of relational powers to positive multiples of N is a subset to the transitive closure raised to the power of N . (Contributed by RP, 15-Jun-2020)

		Ref	Expression
	Assertion	trclrelexplem	$⊢ N \in ℕ \to ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} N) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} N$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = 1 \to (D ↑_{r} k) ↑_{r} x = (D ↑_{r} k) ↑_{r} 1$
2	1	iuneq2d	$⊢ x = 1 \to ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} x) = ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} 1)$
3		oveq2	$⊢ x = 1 \to ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} x = ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} 1$
4	2 3	sseq12d	$⊢ x = 1 \to (⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} x) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} x \leftrightarrow ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} 1) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} 1)$
5		oveq2	$⊢ x = y \to (D ↑_{r} k) ↑_{r} x = (D ↑_{r} k) ↑_{r} y$
6	5	iuneq2d	$⊢ x = y \to ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} x) = ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y)$
7		oveq2	$⊢ x = y \to ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} x = ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y$
8	6 7	sseq12d	$⊢ x = y \to (⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} x) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} x \leftrightarrow ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y)$
9		oveq2	$⊢ x = y + 1 \to (D ↑_{r} k) ↑_{r} x = (D ↑_{r} k) ↑_{r} (y + 1)$
10	9	iuneq2d	$⊢ x = y + 1 \to ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} x) = ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} (y + 1))$
11		oveq2	$⊢ x = y + 1 \to ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} x = ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} (y + 1)$
12	10 11	sseq12d	$⊢ x = y + 1 \to (⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} x) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} x \leftrightarrow ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} (y + 1)) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} (y + 1))$
13		oveq2	$⊢ x = N \to (D ↑_{r} k) ↑_{r} x = (D ↑_{r} k) ↑_{r} N$
14	13	iuneq2d	$⊢ x = N \to ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} x) = ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} N)$
15		oveq2	$⊢ x = N \to ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} x = ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} N$
16	14 15	sseq12d	$⊢ x = N \to (⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} x) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} x \leftrightarrow ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} N) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} N)$
17		oveq2	$⊢ k = l \to D ↑_{r} k = D ↑_{r} l$
18	17	cbviunv	$⊢ ⋃_{k \in ℕ} (D ↑_{r} k) = ⋃_{l \in ℕ} (D ↑_{r} l)$
19		oveq2	$⊢ l = j \to D ↑_{r} l = D ↑_{r} j$
20	19	cbviunv	$⊢ ⋃_{l \in ℕ} (D ↑_{r} l) = ⋃_{j \in ℕ} (D ↑_{r} j)$
21	18 20	eqtri	$⊢ ⋃_{k \in ℕ} (D ↑_{r} k) = ⋃_{j \in ℕ} (D ↑_{r} j)$
22		ovex	$⊢ D ↑_{r} k \in V$
23		relexp1g	$⊢ D ↑_{r} k \in V \to (D ↑_{r} k) ↑_{r} 1 = D ↑_{r} k$
24	22 23	mp1i	$⊢ k \in ℕ \to (D ↑_{r} k) ↑_{r} 1 = D ↑_{r} k$
25	24	iuneq2i	$⊢ ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} 1) = ⋃_{k \in ℕ} (D ↑_{r} k)$
26		nnex	$⊢ ℕ \in V$
27		ovex	$⊢ D ↑_{r} j \in V$
28	26 27	iunex	$⊢ ⋃_{j \in ℕ} (D ↑_{r} j) \in V$
29		relexp1g	$⊢ ⋃_{j \in ℕ} (D ↑_{r} j) \in V \to ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} 1 = ⋃_{j \in ℕ} (D ↑_{r} j)$
30	28 29	ax-mp	$⊢ ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} 1 = ⋃_{j \in ℕ} (D ↑_{r} j)$
31	21 25 30	3eqtr4i	$⊢ ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} 1) = ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} 1$
32	31	eqimssi	$⊢ ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} 1) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} 1$
33		oveq2	$⊢ k = m \to D ↑_{r} k = D ↑_{r} m$
34	33	oveq1d	$⊢ k = m \to (D ↑_{r} k) ↑_{r} y = (D ↑_{r} m) ↑_{r} y$
35	34 33	coeq12d	$⊢ k = m \to ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} k) = ((D ↑_{r} m) ↑_{r} y) \circ (D ↑_{r} m)$
36	35	cbviunv	$⊢ ⋃_{k \in ℕ} (((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} k)) = ⋃_{m \in ℕ} (((D ↑_{r} m) ↑_{r} y) \circ (D ↑_{r} m))$
37		ss2iun	$⊢ \forall m \in ℕ ((D ↑_{r} m) ↑_{r} y) \circ (D ↑_{r} m) \subseteq ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} m) \to ⋃_{m \in ℕ} (((D ↑_{r} m) ↑_{r} y) \circ (D ↑_{r} m)) \subseteq ⋃_{m \in ℕ} (⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} m))$
38	34	ssiun2s	$⊢ m \in ℕ \to (D ↑_{r} m) ↑_{r} y \subseteq ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y)$
39		coss1	$⊢ (D ↑_{r} m) ↑_{r} y \subseteq ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \to ((D ↑_{r} m) ↑_{r} y) \circ (D ↑_{r} m) \subseteq ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} m)$
40	38 39	syl	$⊢ m \in ℕ \to ((D ↑_{r} m) ↑_{r} y) \circ (D ↑_{r} m) \subseteq ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} m)$
41	37 40	mprg	$⊢ ⋃_{m \in ℕ} (((D ↑_{r} m) ↑_{r} y) \circ (D ↑_{r} m)) \subseteq ⋃_{m \in ℕ} (⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} m))$
42	36 41	eqsstri	$⊢ ⋃_{k \in ℕ} (((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} k)) \subseteq ⋃_{m \in ℕ} (⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} m))$
43		coss1	$⊢ ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y \to ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} m) \subseteq (⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ (D ↑_{r} m)$
44	43	ralrimivw	$⊢ ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y \to \forall m \in ℕ ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} m) \subseteq (⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ (D ↑_{r} m)$
45		ss2iun	$⊢ \forall m \in ℕ ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} m) \subseteq (⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ (D ↑_{r} m) \to ⋃_{m \in ℕ} (⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} m)) \subseteq ⋃_{m \in ℕ} ((⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ (D ↑_{r} m))$
46	44 45	syl	$⊢ ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y \to ⋃_{m \in ℕ} (⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} m)) \subseteq ⋃_{m \in ℕ} ((⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ (D ↑_{r} m))$
47	42 46	sstrid	$⊢ ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y \to ⋃_{k \in ℕ} (((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} k)) \subseteq ⋃_{m \in ℕ} ((⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ (D ↑_{r} m))$
48	47	adantl	$⊢ (y \in ℕ \land ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \to ⋃_{k \in ℕ} (((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} k)) \subseteq ⋃_{m \in ℕ} ((⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ (D ↑_{r} m))$
49		relexpsucnnr	$⊢ (D ↑_{r} k \in V \land y \in ℕ) \to (D ↑_{r} k) ↑_{r} (y + 1) = ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} k)$
50	22 49	mpan	$⊢ y \in ℕ \to (D ↑_{r} k) ↑_{r} (y + 1) = ((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} k)$
51	50	iuneq2d	$⊢ y \in ℕ \to ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} (y + 1)) = ⋃_{k \in ℕ} (((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} k))$
52	51	adantr	$⊢ (y \in ℕ \land ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \to ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} (y + 1)) = ⋃_{k \in ℕ} (((D ↑_{r} k) ↑_{r} y) \circ (D ↑_{r} k))$
53		relexpsucnnr	$⊢ (⋃_{j \in ℕ} (D ↑_{r} j) \in V \land y \in ℕ) \to ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} (y + 1) = (⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ ⋃_{j \in ℕ} (D ↑_{r} j)$
54	28 53	mpan	$⊢ y \in ℕ \to ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} (y + 1) = (⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ ⋃_{j \in ℕ} (D ↑_{r} j)$
55		oveq2	$⊢ j = m \to D ↑_{r} j = D ↑_{r} m$
56	55	cbviunv	$⊢ ⋃_{j \in ℕ} (D ↑_{r} j) = ⋃_{m \in ℕ} (D ↑_{r} m)$
57	56	coeq2i	$⊢ (⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ ⋃_{j \in ℕ} (D ↑_{r} j) = (⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ ⋃_{m \in ℕ} (D ↑_{r} m)$
58		coiun	$⊢ (⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ ⋃_{m \in ℕ} (D ↑_{r} m) = ⋃_{m \in ℕ} ((⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ (D ↑_{r} m))$
59	57 58	eqtri	$⊢ (⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ ⋃_{j \in ℕ} (D ↑_{r} j) = ⋃_{m \in ℕ} ((⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ (D ↑_{r} m))$
60	54 59	eqtrdi	$⊢ y \in ℕ \to ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} (y + 1) = ⋃_{m \in ℕ} ((⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ (D ↑_{r} m))$
61	60	adantr	$⊢ (y \in ℕ \land ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \to ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} (y + 1) = ⋃_{m \in ℕ} ((⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \circ (D ↑_{r} m))$
62	48 52 61	3sstr4d	$⊢ (y \in ℕ \land ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y) \to ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} (y + 1)) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} (y + 1)$
63	62	ex	$⊢ y \in ℕ \to (⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} y) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} y \to ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} (y + 1)) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} (y + 1))$
64	4 8 12 16 32 63	nnind	$⊢ N \in ℕ \to ⋃_{k \in ℕ} ((D ↑_{r} k) ↑_{r} N) \subseteq ⋃_{j \in ℕ} (D ↑_{r} j) ↑_{r} N$

Metamath Proof Explorer

Theorem trclrelexplem

Proof