cotrclrcl

Description: The composition of the reflexive and transitive closures is the reflexive-transitive closure. (Contributed by RP, 21-Jun-2020)

		Ref	Expression
	Assertion	cotrclrcl	$⊢ t+ \circ r* = t*$

Proof

Step	Hyp	Ref	Expression
1		dftrcl3	$⊢ t+ = (a \in V ⟼ ⋃_{i \in ℕ} (a ↑_{r} i))$
2		dfrcl4	$⊢ r* = (b \in V ⟼ ⋃_{j \in \{0, 1\}} (b ↑_{r} j))$
3		dfrtrcl3	$⊢ t* = (c \in V ⟼ ⋃_{k \in ℕ_{0}} (c ↑_{r} k))$
4		nnex	$⊢ ℕ \in V$
5		prex	$⊢ \{0, 1\} \in V$
6		df-n0	$⊢ ℕ_{0} = ℕ \cup \{0\}$
7		df-pr	$⊢ \{0, 1\} = \{0\} \cup \{1\}$
8	7	equncomi	$⊢ \{0, 1\} = \{1\} \cup \{0\}$
9	8	uneq2i	$⊢ ℕ \cup \{0, 1\} = ℕ \cup (\{1\} \cup \{0\})$
10		unass	$⊢ (ℕ \cup \{1\}) \cup \{0\} = ℕ \cup (\{1\} \cup \{0\})$
11		1nn	$⊢ 1 \in ℕ$
12		snssi	$⊢ 1 \in ℕ \to \{1\} \subseteq ℕ$
13	11 12	ax-mp	$⊢ \{1\} \subseteq ℕ$
14		ssequn2	$⊢ \{1\} \subseteq ℕ \leftrightarrow ℕ \cup \{1\} = ℕ$
15	13 14	mpbi	$⊢ ℕ \cup \{1\} = ℕ$
16	15	uneq1i	$⊢ (ℕ \cup \{1\}) \cup \{0\} = ℕ \cup \{0\}$
17	9 10 16	3eqtr2ri	$⊢ ℕ \cup \{0\} = ℕ \cup \{0, 1\}$
18	6 17	eqtri	$⊢ ℕ_{0} = ℕ \cup \{0, 1\}$
19		oveq2	$⊢ k = i \to d ↑_{r} k = d ↑_{r} i$
20	19	cbviunv	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) = ⋃_{i \in ℕ} (d ↑_{r} i)$
21		ss2iun	$⊢ \forall i \in ℕ d ↑_{r} i \subseteq ⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i \to ⋃_{i \in ℕ} (d ↑_{r} i) \subseteq ⋃_{i \in ℕ} (⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i)$
22		1elpr01	$⊢ 1 \in \{0, 1\}$
23		oveq2	$⊢ j = 1 \to d ↑_{r} j = d ↑_{r} 1$
24		relexp1g	$⊢ d \in V \to d ↑_{r} 1 = d$
25	24	elv	$⊢ d ↑_{r} 1 = d$
26	23 25	eqtrdi	$⊢ j = 1 \to d ↑_{r} j = d$
27	26	ssiun2s	$⊢ 1 \in \{0, 1\} \to d \subseteq ⋃_{j \in \{0, 1\}} (d ↑_{r} j)$
28	22 27	ax-mp	$⊢ d \subseteq ⋃_{j \in \{0, 1\}} (d ↑_{r} j)$
29	28	a1i	$⊢ i \in ℕ \to d \subseteq ⋃_{j \in \{0, 1\}} (d ↑_{r} j)$
30		ovex	$⊢ d ↑_{r} j \in V$
31	5 30	iunex	$⊢ ⋃_{j \in \{0, 1\}} (d ↑_{r} j) \in V$
32	31	a1i	$⊢ i \in ℕ \to ⋃_{j \in \{0, 1\}} (d ↑_{r} j) \in V$
33		nnnn0	$⊢ i \in ℕ \to i \in ℕ_{0}$
34	29 32 33	relexpss1d	$⊢ i \in ℕ \to d ↑_{r} i \subseteq ⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i$
35	21 34	mprg	$⊢ ⋃_{i \in ℕ} (d ↑_{r} i) \subseteq ⋃_{i \in ℕ} (⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i)$
36	20 35	eqsstri	$⊢ ⋃_{k \in ℕ} (d ↑_{r} k) \subseteq ⋃_{i \in ℕ} (⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i)$
37		oveq2	$⊢ i = 1 \to ⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i = ⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} 1$
38		relexp1g	$⊢ ⋃_{j \in \{0, 1\}} (d ↑_{r} j) \in V \to ⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} 1 = ⋃_{j \in \{0, 1\}} (d ↑_{r} j)$
39	31 38	ax-mp	$⊢ ⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} 1 = ⋃_{j \in \{0, 1\}} (d ↑_{r} j)$
40		oveq2	$⊢ j = k \to d ↑_{r} j = d ↑_{r} k$
41	40	cbviunv	$⊢ ⋃_{j \in \{0, 1\}} (d ↑_{r} j) = ⋃_{k \in \{0, 1\}} (d ↑_{r} k)$
42	39 41	eqtri	$⊢ ⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} 1 = ⋃_{k \in \{0, 1\}} (d ↑_{r} k)$
43	37 42	eqtrdi	$⊢ i = 1 \to ⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i = ⋃_{k \in \{0, 1\}} (d ↑_{r} k)$
44	43	ssiun2s	$⊢ 1 \in ℕ \to ⋃_{k \in \{0, 1\}} (d ↑_{r} k) \subseteq ⋃_{i \in ℕ} (⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i)$
45	11 44	ax-mp	$⊢ ⋃_{k \in \{0, 1\}} (d ↑_{r} k) \subseteq ⋃_{i \in ℕ} (⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i)$
46		iunss	$⊢ ⋃_{i \in ℕ} (⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \leftrightarrow \forall i \in ℕ ⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
47		iuneq1	$⊢ \{0, 1\} = \{0\} \cup \{1\} \to ⋃_{j \in \{0, 1\}} (d ↑_{r} j) = ⋃_{j \in \{0\} \cup \{1\}} (d ↑_{r} j)$
48	7 47	ax-mp	$⊢ ⋃_{j \in \{0, 1\}} (d ↑_{r} j) = ⋃_{j \in \{0\} \cup \{1\}} (d ↑_{r} j)$
49		iunxun	$⊢ ⋃_{j \in \{0\} \cup \{1\}} (d ↑_{r} j) = ⋃_{j \in \{0\}} (d ↑_{r} j) \cup ⋃_{j \in \{1\}} (d ↑_{r} j)$
50		c0ex	$⊢ 0 \in V$
51		oveq2	$⊢ j = 0 \to d ↑_{r} j = d ↑_{r} 0$
52	50 51	iunxsn	$⊢ ⋃_{j \in \{0\}} (d ↑_{r} j) = d ↑_{r} 0$
53		1ex	$⊢ 1 \in V$
54	53 23	iunxsn	$⊢ ⋃_{j \in \{1\}} (d ↑_{r} j) = d ↑_{r} 1$
55	52 54	uneq12i	$⊢ ⋃_{j \in \{0\}} (d ↑_{r} j) \cup ⋃_{j \in \{1\}} (d ↑_{r} j) = (d ↑_{r} 0) \cup (d ↑_{r} 1)$
56	48 49 55	3eqtri	$⊢ ⋃_{j \in \{0, 1\}} (d ↑_{r} j) = (d ↑_{r} 0) \cup (d ↑_{r} 1)$
57	56	oveq1i	$⊢ ⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i = ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} i$
58		oveq2	$⊢ x = 1 \to ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} x = ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} 1$
59	58	sseq1d	$⊢ x = 1 \to (((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} x \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \leftrightarrow ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} 1 \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k))$
60		oveq2	$⊢ x = y \to ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} x = ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y$
61	60	sseq1d	$⊢ x = y \to (((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} x \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \leftrightarrow ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k))$
62		oveq2	$⊢ x = y + 1 \to ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} x = ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} (y + 1)$
63	62	sseq1d	$⊢ x = y + 1 \to (((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} x \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \leftrightarrow ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} (y + 1) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k))$
64		oveq2	$⊢ x = i \to ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} x = ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} i$
65	64	sseq1d	$⊢ x = i \to (((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} x \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \leftrightarrow ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} i \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k))$
66		ovex	$⊢ d ↑_{r} 0 \in V$
67		ovex	$⊢ d ↑_{r} 1 \in V$
68	66 67	unex	$⊢ (d ↑_{r} 0) \cup (d ↑_{r} 1) \in V$
69		relexp1g	$⊢ (d ↑_{r} 0) \cup (d ↑_{r} 1) \in V \to ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} 1 = (d ↑_{r} 0) \cup (d ↑_{r} 1)$
70	68 69	ax-mp	$⊢ ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} 1 = (d ↑_{r} 0) \cup (d ↑_{r} 1)$
71		0nn0	$⊢ 0 \in ℕ_{0}$
72		oveq2	$⊢ k = 0 \to d ↑_{r} k = d ↑_{r} 0$
73	72	ssiun2s	$⊢ 0 \in ℕ_{0} \to d ↑_{r} 0 \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
74	71 73	ax-mp	$⊢ d ↑_{r} 0 \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
75		1nn0	$⊢ 1 \in ℕ_{0}$
76		oveq2	$⊢ k = 1 \to d ↑_{r} k = d ↑_{r} 1$
77	76	ssiun2s	$⊢ 1 \in ℕ_{0} \to d ↑_{r} 1 \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
78	75 77	ax-mp	$⊢ d ↑_{r} 1 \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
79	74 78	unssi	$⊢ (d ↑_{r} 0) \cup (d ↑_{r} 1) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
80	70 79	eqsstri	$⊢ ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} 1 \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
81		simpl	$⊢ (y \in ℕ \land ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)) \to y \in ℕ$
82		relexpsucnnr	$⊢ ((d ↑_{r} 0) \cup (d ↑_{r} 1) \in V \land y \in ℕ) \to ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} (y + 1) = (((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y) \circ ((d ↑_{r} 0) \cup (d ↑_{r} 1))$
83	68 81 82	sylancr	$⊢ (y \in ℕ \land ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)) \to ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} (y + 1) = (((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y) \circ ((d ↑_{r} 0) \cup (d ↑_{r} 1))$
84		coss1	$⊢ ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \to (((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y) \circ ((d ↑_{r} 0) \cup (d ↑_{r} 1)) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ ((d ↑_{r} 0) \cup (d ↑_{r} 1))$
85		coundi	$⊢ ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ ((d ↑_{r} 0) \cup (d ↑_{r} 1)) = (⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ (d ↑_{r} 0)) \cup (⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ (d ↑_{r} 1))$
86		relexp0g	$⊢ d \in V \to d ↑_{r} 0 = {I ↾}_{(dom d \cup ran d)}$
87	86	elv	$⊢ d ↑_{r} 0 = {I ↾}_{(dom d \cup ran d)}$
88	87	coeq2i	$⊢ ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ (d ↑_{r} 0) = ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ ({I ↾}_{(dom d \cup ran d)})$
89		coiun1	$⊢ ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ ({I ↾}_{(dom d \cup ran d)}) = ⋃_{k \in ℕ_{0}} ((d ↑_{r} k) \circ ({I ↾}_{(dom d \cup ran d)}))$
90		coires1	$⊢ (d ↑_{r} k) \circ ({I ↾}_{(dom d \cup ran d)}) = {(d ↑_{r} k) ↾}_{(dom d \cup ran d)}$
91	90	a1i	$⊢ k \in ℕ_{0} \to (d ↑_{r} k) \circ ({I ↾}_{(dom d \cup ran d)}) = {(d ↑_{r} k) ↾}_{(dom d \cup ran d)}$
92	91	iuneq2i	$⊢ ⋃_{k \in ℕ_{0}} ((d ↑_{r} k) \circ ({I ↾}_{(dom d \cup ran d)})) = ⋃_{k \in ℕ_{0}} ({(d ↑_{r} k) ↾}_{(dom d \cup ran d)})$
93	88 89 92	3eqtri	$⊢ ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ (d ↑_{r} 0) = ⋃_{k \in ℕ_{0}} ({(d ↑_{r} k) ↾}_{(dom d \cup ran d)})$
94		ss2iun	$⊢ \forall k \in ℕ_{0} {(d ↑_{r} k) ↾}_{(dom d \cup ran d)} \subseteq d ↑_{r} k \to ⋃_{k \in ℕ_{0}} ({(d ↑_{r} k) ↾}_{(dom d \cup ran d)}) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
95		resss	$⊢ {(d ↑_{r} k) ↾}_{(dom d \cup ran d)} \subseteq d ↑_{r} k$
96	95	a1i	$⊢ k \in ℕ_{0} \to {(d ↑_{r} k) ↾}_{(dom d \cup ran d)} \subseteq d ↑_{r} k$
97	94 96	mprg	$⊢ ⋃_{k \in ℕ_{0}} ({(d ↑_{r} k) ↾}_{(dom d \cup ran d)}) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
98	93 97	eqsstri	$⊢ ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ (d ↑_{r} 0) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
99		coiun1	$⊢ ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ (d ↑_{r} 1) = ⋃_{k \in ℕ_{0}} ((d ↑_{r} k) \circ (d ↑_{r} 1))$
100		iunss2	$⊢ \forall k \in ℕ_{0} \exists i \in ℕ_{0} (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} i \to ⋃_{k \in ℕ_{0}} ((d ↑_{r} k) \circ (d ↑_{r} 1)) \subseteq ⋃_{i \in ℕ_{0}} (d ↑_{r} i)$
101		peano2nn0	$⊢ k \in ℕ_{0} \to k + 1 \in ℕ_{0}$
102		sbcel1v	$⊢ \underset{˙}{[} (k + 1) / i \underset{˙}{]} i \in ℕ_{0} \leftrightarrow k + 1 \in ℕ_{0}$
103	101 102	sylibr	$⊢ k \in ℕ_{0} \to \underset{˙}{[} (k + 1) / i \underset{˙}{]} i \in ℕ_{0}$
104		vex	$⊢ d \in V$
105		relexpaddss	$⊢ (k \in ℕ_{0} \land 1 \in ℕ_{0} \land d \in V) \to (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} (k + 1)$
106	75 104 105	mp3an23	$⊢ k \in ℕ_{0} \to (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} (k + 1)$
107		ovex	$⊢ k + 1 \in V$
108		csbconstg	$⊢ k + 1 \in V \to ⦋ (k + 1) / i ⦌ ((d ↑_{r} k) \circ (d ↑_{r} 1)) = (d ↑_{r} k) \circ (d ↑_{r} 1)$
109	107 108	ax-mp	$⊢ ⦋ (k + 1) / i ⦌ ((d ↑_{r} k) \circ (d ↑_{r} 1)) = (d ↑_{r} k) \circ (d ↑_{r} 1)$
110		csbov2g	$⊢ k + 1 \in V \to ⦋ (k + 1) / i ⦌ (d ↑_{r} i) = d ↑_{r} ⦋ (k + 1) / i ⦌ i$
111		csbvarg	$⊢ k + 1 \in V \to ⦋ (k + 1) / i ⦌ i = k + 1$
112	111	oveq2d	$⊢ k + 1 \in V \to d ↑_{r} ⦋ (k + 1) / i ⦌ i = d ↑_{r} (k + 1)$
113	110 112	eqtrd	$⊢ k + 1 \in V \to ⦋ (k + 1) / i ⦌ (d ↑_{r} i) = d ↑_{r} (k + 1)$
114	107 113	ax-mp	$⊢ ⦋ (k + 1) / i ⦌ (d ↑_{r} i) = d ↑_{r} (k + 1)$
115	106 109 114	3sstr4g	$⊢ k \in ℕ_{0} \to ⦋ (k + 1) / i ⦌ ((d ↑_{r} k) \circ (d ↑_{r} 1)) \subseteq ⦋ (k + 1) / i ⦌ (d ↑_{r} i)$
116		sbcssg	$⊢ k + 1 \in V \to (\underset{˙}{[} (k + 1) / i \underset{˙}{]} (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} i \leftrightarrow ⦋ (k + 1) / i ⦌ ((d ↑_{r} k) \circ (d ↑_{r} 1)) \subseteq ⦋ (k + 1) / i ⦌ (d ↑_{r} i))$
117	107 116	ax-mp	$⊢ \underset{˙}{[} (k + 1) / i \underset{˙}{]} (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} i \leftrightarrow ⦋ (k + 1) / i ⦌ ((d ↑_{r} k) \circ (d ↑_{r} 1)) \subseteq ⦋ (k + 1) / i ⦌ (d ↑_{r} i)$
118	115 117	sylibr	$⊢ k \in ℕ_{0} \to \underset{˙}{[} (k + 1) / i \underset{˙}{]} (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} i$
119		sbcan	$⊢ \underset{˙}{[} (k + 1) / i \underset{˙}{]} (i \in ℕ_{0} \land (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} i) \leftrightarrow (\underset{˙}{[} (k + 1) / i \underset{˙}{]} i \in ℕ_{0} \land \underset{˙}{[} (k + 1) / i \underset{˙}{]} (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} i)$
120	103 118 119	sylanbrc	$⊢ k \in ℕ_{0} \to \underset{˙}{[} (k + 1) / i \underset{˙}{]} (i \in ℕ_{0} \land (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} i)$
121	120	spesbcd	$⊢ k \in ℕ_{0} \to \exists i (i \in ℕ_{0} \land (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} i)$
122		df-rex	$⊢ \exists i \in ℕ_{0} (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} i \leftrightarrow \exists i (i \in ℕ_{0} \land (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} i)$
123	121 122	sylibr	$⊢ k \in ℕ_{0} \to \exists i \in ℕ_{0} (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq d ↑_{r} i$
124	100 123	mprg	$⊢ ⋃_{k \in ℕ_{0}} ((d ↑_{r} k) \circ (d ↑_{r} 1)) \subseteq ⋃_{i \in ℕ_{0}} (d ↑_{r} i)$
125	99 124	eqsstri	$⊢ ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq ⋃_{i \in ℕ_{0}} (d ↑_{r} i)$
126		oveq2	$⊢ i = k \to d ↑_{r} i = d ↑_{r} k$
127	126	cbviunv	$⊢ ⋃_{i \in ℕ_{0}} (d ↑_{r} i) = ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
128	125 127	sseqtri	$⊢ ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ (d ↑_{r} 1) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
129	98 128	unssi	$⊢ (⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ (d ↑_{r} 0)) \cup (⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ (d ↑_{r} 1)) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
130	85 129	eqsstri	$⊢ ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \circ ((d ↑_{r} 0) \cup (d ↑_{r} 1)) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
131	84 130	sstrdi	$⊢ ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \to (((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y) \circ ((d ↑_{r} 0) \cup (d ↑_{r} 1)) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
132	131	adantl	$⊢ (y \in ℕ \land ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)) \to (((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y) \circ ((d ↑_{r} 0) \cup (d ↑_{r} 1)) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
133	83 132	eqsstrd	$⊢ (y \in ℕ \land ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)) \to ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} (y + 1) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
134	133	ex	$⊢ y \in ℕ \to (((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} y \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k) \to ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} (y + 1) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k))$
135	59 61 63 65 80 134	nnind	$⊢ i \in ℕ \to ((d ↑_{r} 0) \cup (d ↑_{r} 1)) ↑_{r} i \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
136	57 135	eqsstrid	$⊢ i \in ℕ \to ⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
137	46 136	mprgbir	$⊢ ⋃_{i \in ℕ} (⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i) \subseteq ⋃_{k \in ℕ_{0}} (d ↑_{r} k)$
138		iuneq1	$⊢ ℕ_{0} = ℕ \cup \{0, 1\} \to ⋃_{k \in ℕ_{0}} (d ↑_{r} k) = ⋃_{k \in ℕ \cup \{0, 1\}} (d ↑_{r} k)$
139	18 138	ax-mp	$⊢ ⋃_{k \in ℕ_{0}} (d ↑_{r} k) = ⋃_{k \in ℕ \cup \{0, 1\}} (d ↑_{r} k)$
140	137 139	sseqtri	$⊢ ⋃_{i \in ℕ} (⋃_{j \in \{0, 1\}} (d ↑_{r} j) ↑_{r} i) \subseteq ⋃_{k \in ℕ \cup \{0, 1\}} (d ↑_{r} k)$
141	1 2 3 4 5 18 36 45 140	comptiunov2i	$⊢ t+ \circ r* = t*$

Metamath Proof Explorer

Theorem cotrclrcl

Proof