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 44186

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 44164	. 2 ⊢ t+ = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ ℕ (𝑎↑_𝑟𝑖))
2		dfrcl4 44120	. 2 ⊢ r* = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ {0, 1} (𝑏↑_𝑟𝑗))
3		dfrtrcl3 44177	. 2 ⊢ t* = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ ℕ₀ (𝑐↑_𝑟𝑘))
4		nnex 12171	. 2 ⊢ ℕ ∈ V
5		prex 5367	. 2 ⊢ {0, 1} ∈ V
6		df-n0 12429	. . 3 ⊢ ℕ₀ = (ℕ ∪ {0})
7		df-pr 4558	. . . . . 6 ⊢ {0, 1} = ({0} ∪ {1})
8	7	equncomi 4090	. . . . 5 ⊢ {0, 1} = ({1} ∪ {0})
9	8	uneq2i 4095	. . . 4 ⊢ (ℕ ∪ {0, 1}) = (ℕ ∪ ({1} ∪ {0}))
10		unass 4101	. . . 4 ⊢ ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ ({1} ∪ {0}))
11		1nn 12176	. . . . . . 7 ⊢ 1 ∈ ℕ
12		snssi 4717	. . . . . . 7 ⊢ (1 ∈ ℕ → {1} ⊆ ℕ)
13	11, 12	ax-mp 5	. . . . . 6 ⊢ {1} ⊆ ℕ
14		ssequn2 4118	. . . . . 6 ⊢ ({1} ⊆ ℕ ↔ (ℕ ∪ {1}) = ℕ)
15	13, 14	mpbi 231	. . . . 5 ⊢ (ℕ ∪ {1}) = ℕ
16	15	uneq1i 4094	. . . 4 ⊢ ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ {0})
17	9, 10, 16	3eqtr2ri 2769	. . 3 ⊢ (ℕ ∪ {0}) = (ℕ ∪ {0, 1})
18	6, 17	eqtri 2762	. 2 ⊢ ℕ₀ = (ℕ ∪ {0, 1})
19		oveq2 7364	. . . 4 ⊢ (𝑘 = 𝑖 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟𝑖))
20	19	cbviunv 4968	. . 3 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) = ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖)
21		ss2iun 4940	. . . 4 ⊢ (∀𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) → ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
22		1ex 11131	. . . . . . . 8 ⊢ 1 ∈ V
23	22	prid2 4695	. . . . . . 7 ⊢ 1 ∈ {0, 1}
24		oveq2 7364	. . . . . . . . 9 ⊢ (𝑗 = 1 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟1))
25		relexp1g 14979	. . . . . . . . . 10 ⊢ (𝑑 ∈ V → (𝑑↑_𝑟1) = 𝑑)
26	25	elv 3436	. . . . . . . . 9 ⊢ (𝑑↑_𝑟1) = 𝑑
27	24, 26	eqtrdi 2790	. . . . . . . 8 ⊢ (𝑗 = 1 → (𝑑↑_𝑟𝑗) = 𝑑)
28	27	ssiun2s 4978	. . . . . . 7 ⊢ (1 ∈ {0, 1} → 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
29	23, 28	ax-mp 5	. . . . . 6 ⊢ 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)
30	29	a1i 11	. . . . 5 ⊢ (𝑖 ∈ ℕ → 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
31		ovex 7389	. . . . . . 7 ⊢ (𝑑↑_𝑟𝑗) ∈ V
32	5, 31	iunex 7910	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V
33	32	a1i 11	. . . . 5 ⊢ (𝑖 ∈ ℕ → ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V)
34		nnnn0 12435	. . . . 5 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℕ₀)
35	30, 33, 34	relexpss1d 44149	. . . 4 ⊢ (𝑖 ∈ ℕ → (𝑑↑_𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
36	21, 35	mprg 3059	. . 3 ⊢ ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
37	20, 36	eqsstri 3961	. 2 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
38		oveq2 7364	. . . . 5 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1))
39		relexp1g 14979	. . . . . . 7 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
40	32, 39	ax-mp 5	. . . . . 6 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)
41		oveq2 7364	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟𝑘))
42	41	cbviunv 4968	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘)
43	40, 42	eqtri 2762	. . . . 5 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘)
44	38, 43	eqtrdi 2790	. . . 4 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘))
45	44	ssiun2s 4978	. . 3 ⊢ (1 ∈ ℕ → ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
46	11, 45	ax-mp 5	. 2 ⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
47		iunss 4974	. . . 4 ⊢ (∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ ∀𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
48		iuneq1 4938	. . . . . . . 8 ⊢ ({0, 1} = ({0} ∪ {1}) → ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗))
49	7, 48	ax-mp 5	. . . . . . 7 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗)
50		iunxun 5023	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗) = (∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) ∪ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗))
51		c0ex 11129	. . . . . . . . 9 ⊢ 0 ∈ V
52		oveq2 7364	. . . . . . . . 9 ⊢ (𝑗 = 0 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟0))
53	51, 52	iunxsn 5020	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟0)
54	22, 24	iunxsn 5020	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟1)
55	53, 54	uneq12i 4096	. . . . . . 7 ⊢ (∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) ∪ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗)) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
56	49, 50, 55	3eqtri 2766	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
57	56	oveq1i 7366	. . . . 5 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖)
58		oveq2 7364	. . . . . . 7 ⊢ (𝑥 = 1 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1))
59	58	sseq1d 3946	. . . . . 6 ⊢ (𝑥 = 1 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
60		oveq2 7364	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦))
61	60	sseq1d 3946	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
62		oveq2 7364	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)))
63	62	sseq1d 3946	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
64		oveq2 7364	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖))
65	64	sseq1d 3946	. . . . . 6 ⊢ (𝑥 = 𝑖 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
66		ovex 7389	. . . . . . . . 9 ⊢ (𝑑↑_𝑟0) ∈ V
67		ovex 7389	. . . . . . . . 9 ⊢ (𝑑↑_𝑟1) ∈ V
68	66, 67	unex 7687	. . . . . . . 8 ⊢ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V
69		relexp1g 14979	. . . . . . . 8 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)))
70	68, 69	ax-mp 5	. . . . . . 7 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
71		0nn0 12443	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
72		oveq2 7364	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟0))
73	72	ssiun2s 4978	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ → (𝑑↑_𝑟0) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
74	71, 73	ax-mp 5	. . . . . . . 8 ⊢ (𝑑↑_𝑟0) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
75		1nn0 12444	. . . . . . . . 9 ⊢ 1 ∈ ℕ₀
76		oveq2 7364	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟1))
77	76	ssiun2s 4978	. . . . . . . . 9 ⊢ (1 ∈ ℕ₀ → (𝑑↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
78	75, 77	ax-mp 5	. . . . . . . 8 ⊢ (𝑑↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
79	74, 78	unssi 4120	. . . . . . 7 ⊢ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
80	70, 79	eqsstri 3961	. . . . . 6 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
81		simpl 483	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → 𝑦 ∈ ℕ)
82		relexpsucnnr 14978	. . . . . . . . 9 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V ∧ 𝑦 ∈ ℕ) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) = ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))))
83	68, 81, 82	sylancr 593	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) = ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))))
84		coss1 5797	. . . . . . . . . 10 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))))
85		coundi 6198	. . . . . . . . . . 11 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) = ((∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ∪ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)))
86		relexp0g 14975	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ V → (𝑑↑_𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
87	86	elv 3436	. . . . . . . . . . . . . . 15 ⊢ (𝑑↑_𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑))
88	87	coeq2i 5802	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) = (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
89		coiun1 44096	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
90		coires1 6216	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
91	90	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)))
92	91	iuneq2i 4943	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
93	88, 89, 92	3eqtri 2766	. . . . . . . . . . . . 13 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
94		ss2iun 4940	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘) → ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
95		resss 5953	. . . . . . . . . . . . . . 15 ⊢ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘)
96	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘))
97	94, 96	mprg 3059	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
98	93, 97	eqsstri 3961	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
99		coiun1 44096	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))
100		iunss2 4979	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ ℕ₀ ∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) → ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖))
101		peano2nn0 12468	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
102		sbcel1v 3788	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀ ↔ (𝑘 + 1) ∈ ℕ₀)
103	101, 102	sylibr 235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀)
104		vex 3435	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑑 ∈ V
105		relexpaddss 44162	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 𝑑 ∈ V) → ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟(𝑘 + 1)))
106	75, 104, 105	mp3an23 1461	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟(𝑘 + 1)))
107		ovex 7389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 + 1) ∈ V
108		csbconstg 3850	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)))
109	107, 108	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))
110		csbov2g 7404	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖))
111		csbvarg 4362	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌𝑖 = (𝑘 + 1))
112	111	oveq2d 7372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 + 1) ∈ V → (𝑑↑_𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖) = (𝑑↑_𝑟(𝑘 + 1)))
113	110, 112	eqtrd 2774	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟(𝑘 + 1)))
114	107, 113	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟(𝑘 + 1))
115	106, 109, 114	3sstr4g 3968	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖))
116		sbcssg 4449	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 + 1) ∈ V → ([(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖)))
117	107, 116	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖))
118	115, 117	sylibr 235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖))
119		sbcan 3772	. . . . . . . . . . . . . . . . . 18 ⊢ ([(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)) ↔ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀ ∧ [(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
120	103, 118, 119	sylanbrc 589	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
121	120	spesbcd 3815	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ₀ → ∃𝑖(𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
122		df-rex 3064	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ∃𝑖(𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
123	121, 122	sylibr 235	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → ∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖))
124	100, 123	mprg 3059	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖)
125	99, 124	eqsstri 3961	. . . . . . . . . . . . 13 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖)
126		oveq2 7364	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (𝑑↑_𝑟𝑖) = (𝑑↑_𝑟𝑘))
127	126	cbviunv 4968	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖) = ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
128	125, 127	sseqtri 3963	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
129	98, 128	unssi 4120	. . . . . . . . . . 11 ⊢ ((∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ∪ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
130	85, 129	eqsstri 3961	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
131	84, 130	sstrdi 3927	. . . . . . . . 9 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
132	131	adantl 482	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
133	83, 132	eqsstrd 3949	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
134	133	ex 413	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
135	59, 61, 63, 65, 80, 134	nnind 12183	. . . . 5 ⊢ (𝑖 ∈ ℕ → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
136	57, 135	eqsstrid 3953	. . . 4 ⊢ (𝑖 ∈ ℕ → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
137	47, 136	mprgbir 3060	. . 3 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
138		iuneq1 4938	. . . 4 ⊢ (ℕ₀ = (ℕ ∪ {0, 1}) → ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘))
139	18, 138	ax-mp 5	. . 3 ⊢ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘)
140	137, 139	sseqtri 3963	. 2 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘)
141	1, 2, 3, 4, 5, 18, 37, 46, 140	comptiunov2i 44150	1 ⊢ (t+ ∘ r) = t

Colors of variables: wff setvar class

Syntax hints: ↔ wb 207 ∧ wa 396 = wceq 1547 ∃wex 1786 ∈ wcel 2119 ∃wrex 3063 Vcvv 3431 [wsbc 3723 ⦋csb 3831 ∪ cun 3881 ⊆ wss 3883 {csn 4555 {cpr 4557 ∪ ciun 4921 I cid 5512 dom cdm 5618 ran crn 5619 ↾ cres 5620 ∘ ccom 5622 (class class class)co 7356 0cc0 11029 1c1 11030 + caddc 11032 ℕcn 12165 ℕ₀cn0 12428 t+ctcl 14938 t*crtcl 14939 ↑_𝑟crelexp 14972 r*crcl 44116

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-er 8633 df-en 8884 df-dom 8885 df-sdom 8886 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-2 12235 df-n0 12429 df-z 12516 df-uz 12780 df-seq 13955 df-trcl 14940 df-rtrcl 14941 df-relexp 14973 df-rcl 44117

This theorem is referenced by: cortrclrcl 44187 cotrclrtrcl 44188 cortrclrtrcl 44189

W3C validator