cotrclrcl - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cotrclrcl		Structured version Visualization version GIF version

Theorem cotrclrcl 42479

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

**Assertion**
Ref	Expression
cotrclrcl	⊢ (t+ ∘ r) = t

Proof of Theorem cotrclrcl Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑖 𝑗 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dftrcl3 42457	. 2 ⊢ t+ = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ ℕ (𝑎↑_𝑟𝑖))
2		dfrcl4 42413	. 2 ⊢ r* = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ {0, 1} (𝑏↑_𝑟𝑗))
3		dfrtrcl3 42470	. 2 ⊢ t* = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ ℕ₀ (𝑐↑_𝑟𝑘))
4		nnex 12215	. 2 ⊢ ℕ ∈ V
5		prex 5432	. 2 ⊢ {0, 1} ∈ V
6		df-n0 12470	. . 3 ⊢ ℕ₀ = (ℕ ∪ {0})
7		df-pr 4631	. . . . . 6 ⊢ {0, 1} = ({0} ∪ {1})
8	7	equncomi 4155	. . . . 5 ⊢ {0, 1} = ({1} ∪ {0})
9	8	uneq2i 4160	. . . 4 ⊢ (ℕ ∪ {0, 1}) = (ℕ ∪ ({1} ∪ {0}))
10		unass 4166	. . . 4 ⊢ ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ ({1} ∪ {0}))
11		1nn 12220	. . . . . . 7 ⊢ 1 ∈ ℕ
12		snssi 4811	. . . . . . 7 ⊢ (1 ∈ ℕ → {1} ⊆ ℕ)
13	11, 12	ax-mp 5	. . . . . 6 ⊢ {1} ⊆ ℕ
14		ssequn2 4183	. . . . . 6 ⊢ ({1} ⊆ ℕ ↔ (ℕ ∪ {1}) = ℕ)
15	13, 14	mpbi 229	. . . . 5 ⊢ (ℕ ∪ {1}) = ℕ
16	15	uneq1i 4159	. . . 4 ⊢ ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ {0})
17	9, 10, 16	3eqtr2ri 2768	. . 3 ⊢ (ℕ ∪ {0}) = (ℕ ∪ {0, 1})
18	6, 17	eqtri 2761	. 2 ⊢ ℕ₀ = (ℕ ∪ {0, 1})
19		oveq2 7414	. . . 4 ⊢ (𝑘 = 𝑖 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟𝑖))
20	19	cbviunv 5043	. . 3 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) = ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖)
21		ss2iun 5015	. . . 4 ⊢ (∀𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) → ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
22		1ex 11207	. . . . . . . 8 ⊢ 1 ∈ V
23	22	prid2 4767	. . . . . . 7 ⊢ 1 ∈ {0, 1}
24		oveq2 7414	. . . . . . . . 9 ⊢ (𝑗 = 1 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟1))
25		relexp1g 14970	. . . . . . . . . 10 ⊢ (𝑑 ∈ V → (𝑑↑_𝑟1) = 𝑑)
26	25	elv 3481	. . . . . . . . 9 ⊢ (𝑑↑_𝑟1) = 𝑑
27	24, 26	eqtrdi 2789	. . . . . . . 8 ⊢ (𝑗 = 1 → (𝑑↑_𝑟𝑗) = 𝑑)
28	27	ssiun2s 5051	. . . . . . 7 ⊢ (1 ∈ {0, 1} → 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
29	23, 28	ax-mp 5	. . . . . 6 ⊢ 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)
30	29	a1i 11	. . . . 5 ⊢ (𝑖 ∈ ℕ → 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
31		ovex 7439	. . . . . . 7 ⊢ (𝑑↑_𝑟𝑗) ∈ V
32	5, 31	iunex 7952	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V
33	32	a1i 11	. . . . 5 ⊢ (𝑖 ∈ ℕ → ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V)
34		nnnn0 12476	. . . . 5 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℕ₀)
35	30, 33, 34	relexpss1d 42442	. . . 4 ⊢ (𝑖 ∈ ℕ → (𝑑↑_𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
36	21, 35	mprg 3068	. . 3 ⊢ ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
37	20, 36	eqsstri 4016	. 2 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
38		oveq2 7414	. . . . 5 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1))
39		relexp1g 14970	. . . . . . 7 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
40	32, 39	ax-mp 5	. . . . . 6 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)
41		oveq2 7414	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟𝑘))
42	41	cbviunv 5043	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘)
43	40, 42	eqtri 2761	. . . . 5 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘)
44	38, 43	eqtrdi 2789	. . . 4 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘))
45	44	ssiun2s 5051	. . 3 ⊢ (1 ∈ ℕ → ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
46	11, 45	ax-mp 5	. 2 ⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
47		iunss 5048	. . . 4 ⊢ (∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ ∀𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
48		iuneq1 5013	. . . . . . . 8 ⊢ ({0, 1} = ({0} ∪ {1}) → ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗))
49	7, 48	ax-mp 5	. . . . . . 7 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗)
50		iunxun 5097	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗) = (∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) ∪ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗))
51		c0ex 11205	. . . . . . . . 9 ⊢ 0 ∈ V
52		oveq2 7414	. . . . . . . . 9 ⊢ (𝑗 = 0 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟0))
53	51, 52	iunxsn 5094	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟0)
54	22, 24	iunxsn 5094	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟1)
55	53, 54	uneq12i 4161	. . . . . . 7 ⊢ (∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) ∪ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗)) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
56	49, 50, 55	3eqtri 2765	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
57	56	oveq1i 7416	. . . . 5 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖)
58		oveq2 7414	. . . . . . 7 ⊢ (𝑥 = 1 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1))
59	58	sseq1d 4013	. . . . . 6 ⊢ (𝑥 = 1 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
60		oveq2 7414	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦))
61	60	sseq1d 4013	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
62		oveq2 7414	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)))
63	62	sseq1d 4013	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
64		oveq2 7414	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖))
65	64	sseq1d 4013	. . . . . 6 ⊢ (𝑥 = 𝑖 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
66		ovex 7439	. . . . . . . . 9 ⊢ (𝑑↑_𝑟0) ∈ V
67		ovex 7439	. . . . . . . . 9 ⊢ (𝑑↑_𝑟1) ∈ V
68	66, 67	unex 7730	. . . . . . . 8 ⊢ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V
69		relexp1g 14970	. . . . . . . 8 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)))
70	68, 69	ax-mp 5	. . . . . . 7 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
71		0nn0 12484	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
72		oveq2 7414	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟0))
73	72	ssiun2s 5051	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ → (𝑑↑_𝑟0) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
74	71, 73	ax-mp 5	. . . . . . . 8 ⊢ (𝑑↑_𝑟0) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
75		1nn0 12485	. . . . . . . . 9 ⊢ 1 ∈ ℕ₀
76		oveq2 7414	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟1))
77	76	ssiun2s 5051	. . . . . . . . 9 ⊢ (1 ∈ ℕ₀ → (𝑑↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
78	75, 77	ax-mp 5	. . . . . . . 8 ⊢ (𝑑↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
79	74, 78	unssi 4185	. . . . . . 7 ⊢ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
80	70, 79	eqsstri 4016	. . . . . 6 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
81		simpl 484	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → 𝑦 ∈ ℕ)
82		relexpsucnnr 14969	. . . . . . . . 9 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V ∧ 𝑦 ∈ ℕ) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) = ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))))
83	68, 81, 82	sylancr 588	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) = ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))))
84		coss1 5854	. . . . . . . . . 10 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))))
85		coundi 6244	. . . . . . . . . . 11 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) = ((∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ∪ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)))
86		relexp0g 14966	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ V → (𝑑↑_𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
87	86	elv 3481	. . . . . . . . . . . . . . 15 ⊢ (𝑑↑_𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑))
88	87	coeq2i 5859	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) = (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
89		coiun1 42389	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
90		coires1 6261	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
91	90	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)))
92	91	iuneq2i 5018	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
93	88, 89, 92	3eqtri 2765	. . . . . . . . . . . . 13 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
94		ss2iun 5015	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘) → ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
95		resss 6005	. . . . . . . . . . . . . . 15 ⊢ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘)
96	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘))
97	94, 96	mprg 3068	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
98	93, 97	eqsstri 4016	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
99		coiun1 42389	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))
100		iunss2 5052	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ ℕ₀ ∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) → ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖))
101		peano2nn0 12509	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
102		sbcel1v 3848	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀ ↔ (𝑘 + 1) ∈ ℕ₀)
103	101, 102	sylibr 233	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀)
104		vex 3479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑑 ∈ V
105		relexpaddss 42455	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 𝑑 ∈ V) → ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟(𝑘 + 1)))
106	75, 104, 105	mp3an23 1454	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟(𝑘 + 1)))
107		ovex 7439	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 + 1) ∈ V
108		csbconstg 3912	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)))
109	107, 108	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))
110		csbov2g 7452	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖))
111		csbvarg 4431	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌𝑖 = (𝑘 + 1))
112	111	oveq2d 7422	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 + 1) ∈ V → (𝑑↑_𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖) = (𝑑↑_𝑟(𝑘 + 1)))
113	110, 112	eqtrd 2773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟(𝑘 + 1)))
114	107, 113	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟(𝑘 + 1))
115	106, 109, 114	3sstr4g 4027	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖))
116		sbcssg 4523	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 + 1) ∈ V → ([(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖)))
117	107, 116	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖))
118	115, 117	sylibr 233	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖))
119		sbcan 3829	. . . . . . . . . . . . . . . . . 18 ⊢ ([(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)) ↔ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀ ∧ [(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
120	103, 118, 119	sylanbrc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
121	120	spesbcd 3877	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ₀ → ∃𝑖(𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
122		df-rex 3072	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ∃𝑖(𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
123	121, 122	sylibr 233	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → ∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖))
124	100, 123	mprg 3068	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖)
125	99, 124	eqsstri 4016	. . . . . . . . . . . . 13 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖)
126		oveq2 7414	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (𝑑↑_𝑟𝑖) = (𝑑↑_𝑟𝑘))
127	126	cbviunv 5043	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖) = ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
128	125, 127	sseqtri 4018	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
129	98, 128	unssi 4185	. . . . . . . . . . 11 ⊢ ((∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ∪ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
130	85, 129	eqsstri 4016	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
131	84, 130	sstrdi 3994	. . . . . . . . 9 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
132	131	adantl 483	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
133	83, 132	eqsstrd 4020	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
134	133	ex 414	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
135	59, 61, 63, 65, 80, 134	nnind 12227	. . . . 5 ⊢ (𝑖 ∈ ℕ → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
136	57, 135	eqsstrid 4030	. . . 4 ⊢ (𝑖 ∈ ℕ → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
137	47, 136	mprgbir 3069	. . 3 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
138		iuneq1 5013	. . . 4 ⊢ (ℕ₀ = (ℕ ∪ {0, 1}) → ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘))
139	18, 138	ax-mp 5	. . 3 ⊢ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘)
140	137, 139	sseqtri 4018	. 2 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘)
141	1, 2, 3, 4, 5, 18, 37, 46, 140	comptiunov2i 42443	1 ⊢ (t+ ∘ r) = t

Colors of variables: wff setvar class

Syntax hints: ↔ wb 205 ∧ wa 397 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ∃wrex 3071 Vcvv 3475 [wsbc 3777 ⦋csb 3893 ∪ cun 3946 ⊆ wss 3948 {csn 4628 {cpr 4630 ∪ ciun 4997 I cid 5573 dom cdm 5676 ran crn 5677 ↾ cres 5678 ∘ ccom 5680 (class class class)co 7406 0cc0 11107 1c1 11108 + caddc 11110 ℕcn 12209 ℕ₀cn0 12469 t+ctcl 14929 t*crtcl 14930 ↑_𝑟crelexp 14963 r*crcl 42409

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-om 7853 df-2nd 7973 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-er 8700 df-en 8937 df-dom 8938 df-sdom 8939 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-nn 12210 df-2 12272 df-n0 12470 df-z 12556 df-uz 12820 df-seq 13964 df-trcl 14931 df-rtrcl 14932 df-relexp 14964 df-rcl 42410

This theorem is referenced by: cortrclrcl 42480 cotrclrtrcl 42481 cortrclrtrcl 42482

W3C validator