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 38034

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 38012	. 2 ⊢ t+ = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ ℕ (𝑎↑_𝑟𝑖))
2		dfrcl4 37968	. 2 ⊢ r* = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ {0, 1} (𝑏↑_𝑟𝑗))
3		dfrtrcl3 38025	. 2 ⊢ t* = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ ℕ₀ (𝑐↑_𝑟𝑘))
4		nnex 11026	. 2 ⊢ ℕ ∈ V
5		prex 4909	. 2 ⊢ {0, 1} ∈ V
6		df-n0 11293	. . 3 ⊢ ℕ₀ = (ℕ ∪ {0})
7		df-pr 4180	. . . . . 6 ⊢ {0, 1} = ({0} ∪ {1})
8	7	equncomi 3759	. . . . 5 ⊢ {0, 1} = ({1} ∪ {0})
9	8	uneq2i 3764	. . . 4 ⊢ (ℕ ∪ {0, 1}) = (ℕ ∪ ({1} ∪ {0}))
10		unass 3770	. . . 4 ⊢ ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ ({1} ∪ {0}))
11		1nn 11031	. . . . . . 7 ⊢ 1 ∈ ℕ
12		snssi 4339	. . . . . . 7 ⊢ (1 ∈ ℕ → {1} ⊆ ℕ)
13	11, 12	ax-mp 5	. . . . . 6 ⊢ {1} ⊆ ℕ
14		ssequn2 3786	. . . . . 6 ⊢ ({1} ⊆ ℕ ↔ (ℕ ∪ {1}) = ℕ)
15	13, 14	mpbi 220	. . . . 5 ⊢ (ℕ ∪ {1}) = ℕ
16	15	uneq1i 3763	. . . 4 ⊢ ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ {0})
17	9, 10, 16	3eqtr2ri 2651	. . 3 ⊢ (ℕ ∪ {0}) = (ℕ ∪ {0, 1})
18	6, 17	eqtri 2644	. 2 ⊢ ℕ₀ = (ℕ ∪ {0, 1})
19		oveq2 6658	. . . 4 ⊢ (𝑘 = 𝑖 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟𝑖))
20	19	cbviunv 4559	. . 3 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) = ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖)
21		ss2iun 4536	. . . 4 ⊢ (∀𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) → ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
22		1ex 10035	. . . . . . . 8 ⊢ 1 ∈ V
23	22	prid2 4298	. . . . . . 7 ⊢ 1 ∈ {0, 1}
24		oveq2 6658	. . . . . . . . 9 ⊢ (𝑗 = 1 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟1))
25		vex 3203	. . . . . . . . . 10 ⊢ 𝑑 ∈ V
26		relexp1g 13766	. . . . . . . . . 10 ⊢ (𝑑 ∈ V → (𝑑↑_𝑟1) = 𝑑)
27	25, 26	ax-mp 5	. . . . . . . . 9 ⊢ (𝑑↑_𝑟1) = 𝑑
28	24, 27	syl6eq 2672	. . . . . . . 8 ⊢ (𝑗 = 1 → (𝑑↑_𝑟𝑗) = 𝑑)
29	28	ssiun2s 4564	. . . . . . 7 ⊢ (1 ∈ {0, 1} → 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
30	23, 29	ax-mp 5	. . . . . 6 ⊢ 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)
31	30	a1i 11	. . . . 5 ⊢ (𝑖 ∈ ℕ → 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
32		ovex 6678	. . . . . . 7 ⊢ (𝑑↑_𝑟𝑗) ∈ V
33	5, 32	iunex 7147	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V
34	33	a1i 11	. . . . 5 ⊢ (𝑖 ∈ ℕ → ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V)
35		nnnn0 11299	. . . . 5 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℕ₀)
36	31, 34, 35	relexpss1d 37997	. . . 4 ⊢ (𝑖 ∈ ℕ → (𝑑↑_𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
37	21, 36	mprg 2926	. . 3 ⊢ ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
38	20, 37	eqsstri 3635	. 2 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
39		oveq2 6658	. . . . 5 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1))
40		relexp1g 13766	. . . . . . 7 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
41	33, 40	ax-mp 5	. . . . . 6 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)
42		oveq2 6658	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟𝑘))
43	42	cbviunv 4559	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘)
44	41, 43	eqtri 2644	. . . . 5 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘)
45	39, 44	syl6eq 2672	. . . 4 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘))
46	45	ssiun2s 4564	. . 3 ⊢ (1 ∈ ℕ → ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
47	11, 46	ax-mp 5	. 2 ⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
48		iunss 4561	. . . 4 ⊢ (∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ ∀𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
49		iuneq1 4534	. . . . . . . 8 ⊢ ({0, 1} = ({0} ∪ {1}) → ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗))
50	7, 49	ax-mp 5	. . . . . . 7 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗)
51		iunxun 4605	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗) = (∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) ∪ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗))
52		c0ex 10034	. . . . . . . . 9 ⊢ 0 ∈ V
53		oveq2 6658	. . . . . . . . 9 ⊢ (𝑗 = 0 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟0))
54	52, 53	iunxsn 4603	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟0)
55	22, 24	iunxsn 4603	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟1)
56	54, 55	uneq12i 3765	. . . . . . 7 ⊢ (∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) ∪ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗)) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
57	50, 51, 56	3eqtri 2648	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
58	57	oveq1i 6660	. . . . 5 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖)
59		oveq2 6658	. . . . . . 7 ⊢ (𝑥 = 1 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1))
60	59	sseq1d 3632	. . . . . 6 ⊢ (𝑥 = 1 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
61		oveq2 6658	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦))
62	61	sseq1d 3632	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
63		oveq2 6658	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)))
64	63	sseq1d 3632	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
65		oveq2 6658	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖))
66	65	sseq1d 3632	. . . . . 6 ⊢ (𝑥 = 𝑖 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
67		ovex 6678	. . . . . . . . 9 ⊢ (𝑑↑_𝑟0) ∈ V
68		ovex 6678	. . . . . . . . 9 ⊢ (𝑑↑_𝑟1) ∈ V
69	67, 68	unex 6956	. . . . . . . 8 ⊢ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V
70		relexp1g 13766	. . . . . . . 8 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)))
71	69, 70	ax-mp 5	. . . . . . 7 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
72		0nn0 11307	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
73		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟0))
74	73	ssiun2s 4564	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ → (𝑑↑_𝑟0) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
75	72, 74	ax-mp 5	. . . . . . . 8 ⊢ (𝑑↑_𝑟0) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
76		1nn0 11308	. . . . . . . . 9 ⊢ 1 ∈ ℕ₀
77		oveq2 6658	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟1))
78	77	ssiun2s 4564	. . . . . . . . 9 ⊢ (1 ∈ ℕ₀ → (𝑑↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
79	76, 78	ax-mp 5	. . . . . . . 8 ⊢ (𝑑↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
80	75, 79	unssi 3788	. . . . . . 7 ⊢ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
81	71, 80	eqsstri 3635	. . . . . 6 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
82		simpl 473	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → 𝑦 ∈ ℕ)
83		relexpsucnnr 13765	. . . . . . . . 9 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V ∧ 𝑦 ∈ ℕ) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) = ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))))
84	69, 82, 83	sylancr 695	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) = ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))))
85		coss1 5277	. . . . . . . . . 10 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))))
86		coundi 5636	. . . . . . . . . . 11 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) = ((∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ∪ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)))
87		relexp0g 13762	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ V → (𝑑↑_𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
88	25, 87	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ (𝑑↑_𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑))
89	88	coeq2i 5282	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) = (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
90		coiun1 37944	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
91		coires1 5653	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
92	91	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)))
93	92	iuneq2i 4539	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
94	89, 90, 93	3eqtri 2648	. . . . . . . . . . . . 13 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
95		ss2iun 4536	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘) → ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
96		resss 5422	. . . . . . . . . . . . . . 15 ⊢ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘)
97	96	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘))
98	95, 97	mprg 2926	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
99	94, 98	eqsstri 3635	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
100		coiun1 37944	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))
101		iunss2 4565	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ ℕ₀ ∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) → ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖))
102		peano2nn0 11333	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
103		sbcel1v 3495	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀ ↔ (𝑘 + 1) ∈ ℕ₀)
104	102, 103	sylibr 224	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀)
105		relexpaddss 38010	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 𝑑 ∈ V) → ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟(𝑘 + 1)))
106	76, 25, 105	mp3an23 1416	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟(𝑘 + 1)))
107		ovex 6678	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 + 1) ∈ V
108		csbconstg 3546	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)))
109	107, 108	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))
110		csbov2g 6691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖))
111		csbvarg 4003	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌𝑖 = (𝑘 + 1))
112	111	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 + 1) ∈ V → (𝑑↑_𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖) = (𝑑↑_𝑟(𝑘 + 1)))
113	110, 112	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟(𝑘 + 1)))
114	107, 113	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟(𝑘 + 1))
115	106, 109, 114	3sstr4g 3646	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖))
116		sbcssg 4085	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 + 1) ∈ V → ([(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖)))
117	107, 116	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖))
118	115, 117	sylibr 224	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖))
119		sbcan 3478	. . . . . . . . . . . . . . . . . 18 ⊢ ([(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)) ↔ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀ ∧ [(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
120	104, 118, 119	sylanbrc 698	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
121	120	spesbcd 3522	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ₀ → ∃𝑖(𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
122		df-rex 2918	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ∃𝑖(𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
123	121, 122	sylibr 224	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → ∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖))
124	101, 123	mprg 2926	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖)
125	100, 124	eqsstri 3635	. . . . . . . . . . . . 13 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖)
126		oveq2 6658	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (𝑑↑_𝑟𝑖) = (𝑑↑_𝑟𝑘))
127	126	cbviunv 4559	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖) = ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
128	125, 127	sseqtri 3637	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
129	99, 128	unssi 3788	. . . . . . . . . . 11 ⊢ ((∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ∪ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
130	86, 129	eqsstri 3635	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
131	85, 130	syl6ss 3615	. . . . . . . . 9 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
132	131	adantl 482	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
133	84, 132	eqsstrd 3639	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
134	133	ex 450	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
135	60, 62, 64, 66, 81, 134	nnind 11038	. . . . 5 ⊢ (𝑖 ∈ ℕ → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
136	58, 135	syl5eqss 3649	. . . 4 ⊢ (𝑖 ∈ ℕ → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
137	48, 136	mprgbir 2927	. . 3 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
138		iuneq1 4534	. . . 4 ⊢ (ℕ₀ = (ℕ ∪ {0, 1}) → ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘))
139	18, 138	ax-mp 5	. . 3 ⊢ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘)
140	137, 139	sseqtri 3637	. 2 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘)
141	1, 2, 3, 4, 5, 18, 38, 47, 140	comptiunov2i 37998	1 ⊢ (t+ ∘ r) = t

Colors of variables: wff setvar class

Syntax hints: ↔ wb 196 ∧ wa 384 = wceq 1483 ∃wex 1704 ∈ wcel 1990 ∃wrex 2913 Vcvv 3200 [wsbc 3435 ⦋csb 3533 ∪ cun 3572 ⊆ wss 3574 {csn 4177 {cpr 4179 ∪ ciun 4520 I cid 5023 dom cdm 5114 ran crn 5115 ↾ cres 5116 ∘ ccom 5118 (class class class)co 6650 0cc0 9936 1c1 9937 + caddc 9939 ℕcn 11020 ℕ₀cn0 11292 t+ctcl 13724 t*crtcl 13725 ↑_𝑟crelexp 13760 r*crcl 37964

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-er 7742 df-en 7956 df-dom 7957 df-sdom 7958 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-nn 11021 df-2 11079 df-n0 11293 df-z 11378 df-uz 11688 df-seq 12802 df-trcl 13726 df-rtrcl 13727 df-relexp 13761 df-rcl 37965

This theorem is referenced by: cortrclrcl 38035 cotrclrtrcl 38036 cortrclrtrcl 38037

W3C validator