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 44169

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 44147	. 2 ⊢ t+ = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ ℕ (𝑎↑_𝑟𝑖))
2		dfrcl4 44103	. 2 ⊢ r* = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ {0, 1} (𝑏↑_𝑟𝑗))
3		dfrtrcl3 44160	. 2 ⊢ t* = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ ℕ₀ (𝑐↑_𝑟𝑘))
4		nnex 12180	. 2 ⊢ ℕ ∈ V
5		prex 5380	. 2 ⊢ {0, 1} ∈ V
6		df-n0 12438	. . 3 ⊢ ℕ₀ = (ℕ ∪ {0})
7		df-pr 4570	. . . . . 6 ⊢ {0, 1} = ({0} ∪ {1})
8	7	equncomi 4100	. . . . 5 ⊢ {0, 1} = ({1} ∪ {0})
9	8	uneq2i 4105	. . . 4 ⊢ (ℕ ∪ {0, 1}) = (ℕ ∪ ({1} ∪ {0}))
10		unass 4112	. . . 4 ⊢ ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ ({1} ∪ {0}))
11		1nn 12185	. . . . . . 7 ⊢ 1 ∈ ℕ
12		snssi 4729	. . . . . . 7 ⊢ (1 ∈ ℕ → {1} ⊆ ℕ)
13	11, 12	ax-mp 5	. . . . . 6 ⊢ {1} ⊆ ℕ
14		ssequn2 4129	. . . . . 6 ⊢ ({1} ⊆ ℕ ↔ (ℕ ∪ {1}) = ℕ)
15	13, 14	mpbi 230	. . . . 5 ⊢ (ℕ ∪ {1}) = ℕ
16	15	uneq1i 4104	. . . 4 ⊢ ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ {0})
17	9, 10, 16	3eqtr2ri 2766	. . 3 ⊢ (ℕ ∪ {0}) = (ℕ ∪ {0, 1})
18	6, 17	eqtri 2759	. 2 ⊢ ℕ₀ = (ℕ ∪ {0, 1})
19		oveq2 7375	. . . 4 ⊢ (𝑘 = 𝑖 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟𝑖))
20	19	cbviunv 4981	. . 3 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) = ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖)
21		ss2iun 4952	. . . 4 ⊢ (∀𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) → ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
22		1ex 11140	. . . . . . . 8 ⊢ 1 ∈ V
23	22	prid2 4707	. . . . . . 7 ⊢ 1 ∈ {0, 1}
24		oveq2 7375	. . . . . . . . 9 ⊢ (𝑗 = 1 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟1))
25		relexp1g 14988	. . . . . . . . . 10 ⊢ (𝑑 ∈ V → (𝑑↑_𝑟1) = 𝑑)
26	25	elv 3434	. . . . . . . . 9 ⊢ (𝑑↑_𝑟1) = 𝑑
27	24, 26	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑗 = 1 → (𝑑↑_𝑟𝑗) = 𝑑)
28	27	ssiun2s 4991	. . . . . . 7 ⊢ (1 ∈ {0, 1} → 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
29	23, 28	ax-mp 5	. . . . . 6 ⊢ 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)
30	29	a1i 11	. . . . 5 ⊢ (𝑖 ∈ ℕ → 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
31		ovex 7400	. . . . . . 7 ⊢ (𝑑↑_𝑟𝑗) ∈ V
32	5, 31	iunex 7921	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V
33	32	a1i 11	. . . . 5 ⊢ (𝑖 ∈ ℕ → ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V)
34		nnnn0 12444	. . . . 5 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℕ₀)
35	30, 33, 34	relexpss1d 44132	. . . 4 ⊢ (𝑖 ∈ ℕ → (𝑑↑_𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
36	21, 35	mprg 3057	. . 3 ⊢ ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
37	20, 36	eqsstri 3968	. 2 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
38		oveq2 7375	. . . . 5 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1))
39		relexp1g 14988	. . . . . . 7 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
40	32, 39	ax-mp 5	. . . . . 6 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)
41		oveq2 7375	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟𝑘))
42	41	cbviunv 4981	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘)
43	40, 42	eqtri 2759	. . . . 5 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘)
44	38, 43	eqtrdi 2787	. . . 4 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘))
45	44	ssiun2s 4991	. . 3 ⊢ (1 ∈ ℕ → ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
46	11, 45	ax-mp 5	. 2 ⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
47		iunss 4987	. . . 4 ⊢ (∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ ∀𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
48		iuneq1 4950	. . . . . . . 8 ⊢ ({0, 1} = ({0} ∪ {1}) → ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗))
49	7, 48	ax-mp 5	. . . . . . 7 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗)
50		iunxun 5036	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗) = (∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) ∪ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗))
51		c0ex 11138	. . . . . . . . 9 ⊢ 0 ∈ V
52		oveq2 7375	. . . . . . . . 9 ⊢ (𝑗 = 0 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟0))
53	51, 52	iunxsn 5033	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟0)
54	22, 24	iunxsn 5033	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟1)
55	53, 54	uneq12i 4106	. . . . . . 7 ⊢ (∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) ∪ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗)) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
56	49, 50, 55	3eqtri 2763	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
57	56	oveq1i 7377	. . . . 5 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖)
58		oveq2 7375	. . . . . . 7 ⊢ (𝑥 = 1 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1))
59	58	sseq1d 3953	. . . . . 6 ⊢ (𝑥 = 1 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
60		oveq2 7375	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦))
61	60	sseq1d 3953	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
62		oveq2 7375	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)))
63	62	sseq1d 3953	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
64		oveq2 7375	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖))
65	64	sseq1d 3953	. . . . . 6 ⊢ (𝑥 = 𝑖 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
66		ovex 7400	. . . . . . . . 9 ⊢ (𝑑↑_𝑟0) ∈ V
67		ovex 7400	. . . . . . . . 9 ⊢ (𝑑↑_𝑟1) ∈ V
68	66, 67	unex 7698	. . . . . . . 8 ⊢ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V
69		relexp1g 14988	. . . . . . . 8 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)))
70	68, 69	ax-mp 5	. . . . . . 7 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
71		0nn0 12452	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
72		oveq2 7375	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟0))
73	72	ssiun2s 4991	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ → (𝑑↑_𝑟0) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
74	71, 73	ax-mp 5	. . . . . . . 8 ⊢ (𝑑↑_𝑟0) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
75		1nn0 12453	. . . . . . . . 9 ⊢ 1 ∈ ℕ₀
76		oveq2 7375	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟1))
77	76	ssiun2s 4991	. . . . . . . . 9 ⊢ (1 ∈ ℕ₀ → (𝑑↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
78	75, 77	ax-mp 5	. . . . . . . 8 ⊢ (𝑑↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
79	74, 78	unssi 4131	. . . . . . 7 ⊢ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
80	70, 79	eqsstri 3968	. . . . . 6 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
81		simpl 482	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → 𝑦 ∈ ℕ)
82		relexpsucnnr 14987	. . . . . . . . 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 5810	. . . . . . . . . 10 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))))
85		coundi 6211	. . . . . . . . . . 11 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) = ((∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ∪ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)))
86		relexp0g 14984	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ V → (𝑑↑_𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
87	86	elv 3434	. . . . . . . . . . . . . . 15 ⊢ (𝑑↑_𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑))
88	87	coeq2i 5815	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) = (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
89		coiun1 44079	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
90		coires1 6229	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
91	90	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)))
92	91	iuneq2i 4955	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
93	88, 89, 92	3eqtri 2763	. . . . . . . . . . . . 13 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
94		ss2iun 4952	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘) → ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
95		resss 5966	. . . . . . . . . . . . . . 15 ⊢ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘)
96	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘))
97	94, 96	mprg 3057	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
98	93, 97	eqsstri 3968	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
99		coiun1 44079	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))
100		iunss2 4992	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ ℕ₀ ∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) → ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖))
101		peano2nn0 12477	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
102		sbcel1v 3794	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀ ↔ (𝑘 + 1) ∈ ℕ₀)
103	101, 102	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀)
104		vex 3433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑑 ∈ V
105		relexpaddss 44145	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 𝑑 ∈ V) → ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟(𝑘 + 1)))
106	75, 104, 105	mp3an23 1456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟(𝑘 + 1)))
107		ovex 7400	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 + 1) ∈ V
108		csbconstg 3856	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)))
109	107, 108	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))
110		csbov2g 7415	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖))
111		csbvarg 4374	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌𝑖 = (𝑘 + 1))
112	111	oveq2d 7383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 + 1) ∈ V → (𝑑↑_𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖) = (𝑑↑_𝑟(𝑘 + 1)))
113	110, 112	eqtrd 2771	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟(𝑘 + 1)))
114	107, 113	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟(𝑘 + 1))
115	106, 109, 114	3sstr4g 3975	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖))
116		sbcssg 4461	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 + 1) ∈ V → ([(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖)))
117	107, 116	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖))
118	115, 117	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖))
119		sbcan 3778	. . . . . . . . . . . . . . . . . 18 ⊢ ([(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)) ↔ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀ ∧ [(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
120	103, 118, 119	sylanbrc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
121	120	spesbcd 3821	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ₀ → ∃𝑖(𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
122		df-rex 3062	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ∃𝑖(𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
123	121, 122	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → ∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖))
124	100, 123	mprg 3057	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖)
125	99, 124	eqsstri 3968	. . . . . . . . . . . . 13 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖)
126		oveq2 7375	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (𝑑↑_𝑟𝑖) = (𝑑↑_𝑟𝑘))
127	126	cbviunv 4981	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖) = ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
128	125, 127	sseqtri 3970	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
129	98, 128	unssi 4131	. . . . . . . . . . 11 ⊢ ((∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ∪ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
130	85, 129	eqsstri 3968	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
131	84, 130	sstrdi 3934	. . . . . . . . 9 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
132	131	adantl 481	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
133	83, 132	eqsstrd 3956	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
134	133	ex 412	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
135	59, 61, 63, 65, 80, 134	nnind 12192	. . . . 5 ⊢ (𝑖 ∈ ℕ → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
136	57, 135	eqsstrid 3960	. . . 4 ⊢ (𝑖 ∈ ℕ → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
137	47, 136	mprgbir 3058	. . 3 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
138		iuneq1 4950	. . . 4 ⊢ (ℕ₀ = (ℕ ∪ {0, 1}) → ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘))
139	18, 138	ax-mp 5	. . 3 ⊢ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘)
140	137, 139	sseqtri 3970	. 2 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘)
141	1, 2, 3, 4, 5, 18, 37, 46, 140	comptiunov2i 44133	1 ⊢ (t+ ∘ r) = t

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ∃wrex 3061 Vcvv 3429 [wsbc 3728 ⦋csb 3837 ∪ cun 3887 ⊆ wss 3889 {csn 4567 {cpr 4569 ∪ ciun 4933 I cid 5525 dom cdm 5631 ran crn 5632 ↾ cres 5633 ∘ ccom 5635 (class class class)co 7367 0cc0 11038 1c1 11039 + caddc 11041 ℕcn 12174 ℕ₀cn0 12437 t+ctcl 14947 t*crtcl 14948 ↑_𝑟crelexp 14981 r*crcl 44099

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-2 12244 df-n0 12438 df-z 12525 df-uz 12789 df-seq 13964 df-trcl 14949 df-rtrcl 14950 df-relexp 14982 df-rcl 44100

This theorem is referenced by: cortrclrcl 44170 cotrclrtrcl 44171 cortrclrtrcl 44172

W3C validator