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 44190

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 44168	. 2 ⊢ t+ = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ ℕ (𝑎↑_𝑟𝑖))
2		dfrcl4 44124	. 2 ⊢ r* = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ {0, 1} (𝑏↑_𝑟𝑗))
3		dfrtrcl3 44181	. 2 ⊢ t* = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ ℕ₀ (𝑐↑_𝑟𝑘))
4		nnex 12174	. 2 ⊢ ℕ ∈ V
5		prex 5376	. 2 ⊢ {0, 1} ∈ V
6		df-n0 12432	. . 3 ⊢ ℕ₀ = (ℕ ∪ {0})
7		df-pr 4571	. . . . . 6 ⊢ {0, 1} = ({0} ∪ {1})
8	7	equncomi 4101	. . . . 5 ⊢ {0, 1} = ({1} ∪ {0})
9	8	uneq2i 4106	. . . 4 ⊢ (ℕ ∪ {0, 1}) = (ℕ ∪ ({1} ∪ {0}))
10		unass 4113	. . . 4 ⊢ ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ ({1} ∪ {0}))
11		1nn 12179	. . . . . . 7 ⊢ 1 ∈ ℕ
12		snssi 4752	. . . . . . 7 ⊢ (1 ∈ ℕ → {1} ⊆ ℕ)
13	11, 12	ax-mp 5	. . . . . 6 ⊢ {1} ⊆ ℕ
14		ssequn2 4130	. . . . . 6 ⊢ ({1} ⊆ ℕ ↔ (ℕ ∪ {1}) = ℕ)
15	13, 14	mpbi 230	. . . . 5 ⊢ (ℕ ∪ {1}) = ℕ
16	15	uneq1i 4105	. . . 4 ⊢ ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ {0})
17	9, 10, 16	3eqtr2ri 2767	. . 3 ⊢ (ℕ ∪ {0}) = (ℕ ∪ {0, 1})
18	6, 17	eqtri 2760	. 2 ⊢ ℕ₀ = (ℕ ∪ {0, 1})
19		oveq2 7369	. . . 4 ⊢ (𝑘 = 𝑖 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟𝑖))
20	19	cbviunv 4982	. . 3 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) = ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖)
21		ss2iun 4953	. . . 4 ⊢ (∀𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) → ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
22		1ex 11134	. . . . . . . 8 ⊢ 1 ∈ V
23	22	prid2 4708	. . . . . . 7 ⊢ 1 ∈ {0, 1}
24		oveq2 7369	. . . . . . . . 9 ⊢ (𝑗 = 1 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟1))
25		relexp1g 14982	. . . . . . . . . 10 ⊢ (𝑑 ∈ V → (𝑑↑_𝑟1) = 𝑑)
26	25	elv 3435	. . . . . . . . 9 ⊢ (𝑑↑_𝑟1) = 𝑑
27	24, 26	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑗 = 1 → (𝑑↑_𝑟𝑗) = 𝑑)
28	27	ssiun2s 4992	. . . . . . 7 ⊢ (1 ∈ {0, 1} → 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
29	23, 28	ax-mp 5	. . . . . 6 ⊢ 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)
30	29	a1i 11	. . . . 5 ⊢ (𝑖 ∈ ℕ → 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
31		ovex 7394	. . . . . . 7 ⊢ (𝑑↑_𝑟𝑗) ∈ V
32	5, 31	iunex 7915	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V
33	32	a1i 11	. . . . 5 ⊢ (𝑖 ∈ ℕ → ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V)
34		nnnn0 12438	. . . . 5 ⊢ (𝑖 ∈ ℕ → 𝑖 ∈ ℕ₀)
35	30, 33, 34	relexpss1d 44153	. . . 4 ⊢ (𝑖 ∈ ℕ → (𝑑↑_𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
36	21, 35	mprg 3058	. . 3 ⊢ ∪ 𝑖 ∈ ℕ (𝑑↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
37	20, 36	eqsstri 3969	. 2 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
38		oveq2 7369	. . . . 5 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1))
39		relexp1g 14982	. . . . . . 7 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) ∈ V → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗))
40	32, 39	ax-mp 5	. . . . . 6 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)
41		oveq2 7369	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟𝑘))
42	41	cbviunv 4982	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘)
43	40, 42	eqtri 2760	. . . . 5 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘)
44	38, 43	eqtrdi 2788	. . . 4 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘))
45	44	ssiun2s 4992	. . 3 ⊢ (1 ∈ ℕ → ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
46	11, 45	ax-mp 5	. 2 ⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
47		iunss 4988	. . . 4 ⊢ (∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ ∀𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
48		iuneq1 4951	. . . . . . . 8 ⊢ ({0, 1} = ({0} ∪ {1}) → ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗))
49	7, 48	ax-mp 5	. . . . . . 7 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗)
50		iunxun 5037	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑_𝑟𝑗) = (∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) ∪ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗))
51		c0ex 11132	. . . . . . . . 9 ⊢ 0 ∈ V
52		oveq2 7369	. . . . . . . . 9 ⊢ (𝑗 = 0 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟0))
53	51, 52	iunxsn 5034	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟0)
54	22, 24	iunxsn 5034	. . . . . . . 8 ⊢ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟1)
55	53, 54	uneq12i 4107	. . . . . . 7 ⊢ (∪ 𝑗 ∈ {0} (𝑑↑_𝑟𝑗) ∪ ∪ 𝑗 ∈ {1} (𝑑↑_𝑟𝑗)) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
56	49, 50, 55	3eqtri 2764	. . . . . 6 ⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
57	56	oveq1i 7371	. . . . 5 ⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖)
58		oveq2 7369	. . . . . . 7 ⊢ (𝑥 = 1 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1))
59	58	sseq1d 3954	. . . . . 6 ⊢ (𝑥 = 1 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
60		oveq2 7369	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦))
61	60	sseq1d 3954	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
62		oveq2 7369	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)))
63	62	sseq1d 3954	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
64		oveq2 7369	. . . . . . 7 ⊢ (𝑥 = 𝑖 → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) = (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖))
65	64	sseq1d 3954	. . . . . 6 ⊢ (𝑥 = 𝑖 → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ↔ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
66		ovex 7394	. . . . . . . . 9 ⊢ (𝑑↑_𝑟0) ∈ V
67		ovex 7394	. . . . . . . . 9 ⊢ (𝑑↑_𝑟1) ∈ V
68	66, 67	unex 7692	. . . . . . . 8 ⊢ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V
69		relexp1g 14982	. . . . . . . 8 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ∈ V → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)))
70	68, 69	ax-mp 5	. . . . . . 7 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) = ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))
71		0nn0 12446	. . . . . . . . 9 ⊢ 0 ∈ ℕ₀
72		oveq2 7369	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟0))
73	72	ssiun2s 4992	. . . . . . . . 9 ⊢ (0 ∈ ℕ₀ → (𝑑↑_𝑟0) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
74	71, 73	ax-mp 5	. . . . . . . 8 ⊢ (𝑑↑_𝑟0) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
75		1nn0 12447	. . . . . . . . 9 ⊢ 1 ∈ ℕ₀
76		oveq2 7369	. . . . . . . . . 10 ⊢ (𝑘 = 1 → (𝑑↑_𝑟𝑘) = (𝑑↑_𝑟1))
77	76	ssiun2s 4992	. . . . . . . . 9 ⊢ (1 ∈ ℕ₀ → (𝑑↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
78	75, 77	ax-mp 5	. . . . . . . 8 ⊢ (𝑑↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
79	74, 78	unssi 4132	. . . . . . 7 ⊢ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
80	70, 79	eqsstri 3969	. . . . . 6 ⊢ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
81		simpl 482	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → 𝑦 ∈ ℕ)
82		relexpsucnnr 14981	. . . . . . . . 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 5805	. . . . . . . . . 10 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))))
85		coundi 6206	. . . . . . . . . . 11 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) = ((∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ∪ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)))
86		relexp0g 14978	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ V → (𝑑↑_𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
87	86	elv 3435	. . . . . . . . . . . . . . 15 ⊢ (𝑑↑_𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑))
88	87	coeq2i 5810	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) = (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
89		coiun1 44100	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
90		coires1 6224	. . . . . . . . . . . . . . . 16 ⊢ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
91	90	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)))
92	91	iuneq2i 4956	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
93	88, 89, 92	3eqtri 2764	. . . . . . . . . . . . 13 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
94		ss2iun 4953	. . . . . . . . . . . . . 14 ⊢ (∀𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘) → ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
95		resss 5961	. . . . . . . . . . . . . . 15 ⊢ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘)
96	95	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑_𝑟𝑘))
97	94, 96	mprg 3058	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
98	93, 97	eqsstri 3969	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
99		coiun1 44100	. . . . . . . . . . . . . 14 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))
100		iunss2 4993	. . . . . . . . . . . . . . 15 ⊢ (∀𝑘 ∈ ℕ₀ ∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) → ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖))
101		peano2nn0 12471	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → (𝑘 + 1) ∈ ℕ₀)
102		sbcel1v 3795	. . . . . . . . . . . . . . . . . . 19 ⊢ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀ ↔ (𝑘 + 1) ∈ ℕ₀)
103	101, 102	sylibr 234	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀)
104		vex 3434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝑑 ∈ V
105		relexpaddss 44166	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 ∈ ℕ₀ ∧ 1 ∈ ℕ₀ ∧ 𝑑 ∈ V) → ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟(𝑘 + 1)))
106	75, 104, 105	mp3an23 1456	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ℕ₀ → ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟(𝑘 + 1)))
107		ovex 7394	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑘 + 1) ∈ V
108		csbconstg 3857	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)))
109	107, 108	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) = ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))
110		csbov2g 7409	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖))
111		csbvarg 4375	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌𝑖 = (𝑘 + 1))
112	111	oveq2d 7377	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑘 + 1) ∈ V → (𝑑↑_𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖) = (𝑑↑_𝑟(𝑘 + 1)))
113	110, 112	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑘 + 1) ∈ V → ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟(𝑘 + 1)))
114	107, 113	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖) = (𝑑↑_𝑟(𝑘 + 1))
115	106, 109, 114	3sstr4g 3976	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑘 ∈ ℕ₀ → ⦋(𝑘 + 1) / 𝑖⦌((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ⦋(𝑘 + 1) / 𝑖⦌(𝑑↑_𝑟𝑖))
116		sbcssg 4462	. . . . . . . . . . . . . . . . . . . 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 3779	. . . . . . . . . . . . . . . . . 18 ⊢ ([(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)) ↔ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ₀ ∧ [(𝑘 + 1) / 𝑖]((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
120	103, 118, 119	sylanbrc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝑘 ∈ ℕ₀ → [(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
121	120	spesbcd 3822	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ ℕ₀ → ∃𝑖(𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
122		df-rex 3063	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖) ↔ ∃𝑖(𝑖 ∈ ℕ₀ ∧ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖)))
123	121, 122	sylibr 234	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℕ₀ → ∃𝑖 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ (𝑑↑_𝑟𝑖))
124	100, 123	mprg 3058	. . . . . . . . . . . . . 14 ⊢ ∪ 𝑘 ∈ ℕ₀ ((𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖)
125	99, 124	eqsstri 3969	. . . . . . . . . . . . 13 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖)
126		oveq2 7369	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (𝑑↑_𝑟𝑖) = (𝑑↑_𝑟𝑘))
127	126	cbviunv 4982	. . . . . . . . . . . . 13 ⊢ ∪ 𝑖 ∈ ℕ₀ (𝑑↑_𝑟𝑖) = ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
128	125, 127	sseqtri 3971	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
129	98, 128	unssi 4132	. . . . . . . . . . 11 ⊢ ((∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟0)) ∪ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
130	85, 129	eqsstri 3969	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
131	84, 130	sstrdi 3935	. . . . . . . . 9 ⊢ ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
132	131	adantl 481	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ∘ ((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
133	83, 132	eqsstrd 3957	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
134	133	ex 412	. . . . . 6 ⊢ (𝑦 ∈ ℕ → ((((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)))
135	59, 61, 63, 65, 80, 134	nnind 12186	. . . . 5 ⊢ (𝑖 ∈ ℕ → (((𝑑↑_𝑟0) ∪ (𝑑↑_𝑟1))↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
136	57, 135	eqsstrid 3961	. . . 4 ⊢ (𝑖 ∈ ℕ → (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘))
137	47, 136	mprgbir 3059	. . 3 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘)
138		iuneq1 4951	. . . 4 ⊢ (ℕ₀ = (ℕ ∪ {0, 1}) → ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘))
139	18, 138	ax-mp 5	. . 3 ⊢ ∪ 𝑘 ∈ ℕ₀ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘)
140	137, 139	sseqtri 3971	. 2 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑_𝑟𝑘)
141	1, 2, 3, 4, 5, 18, 37, 46, 140	comptiunov2i 44154	1 ⊢ (t+ ∘ r) = t

Colors of variables: wff setvar class

Syntax hints: ↔ wb 206 ∧ wa 395 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ∃wrex 3062 Vcvv 3430 [wsbc 3729 ⦋csb 3838 ∪ cun 3888 ⊆ wss 3890 {csn 4568 {cpr 4570 ∪ ciun 4934 I cid 5519 dom cdm 5625 ran crn 5626 ↾ cres 5627 ∘ ccom 5629 (class class class)co 7361 0cc0 11032 1c1 11033 + caddc 11035 ℕcn 12168 ℕ₀cn0 12431 t+ctcl 14941 t*crtcl 14942 ↑_𝑟crelexp 14975 r*crcl 44120

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 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683 ax-cnex 11088 ax-resscn 11089 ax-1cn 11090 ax-icn 11091 ax-addcl 11092 ax-addrcl 11093 ax-mulcl 11094 ax-mulrcl 11095 ax-mulcom 11096 ax-addass 11097 ax-mulass 11098 ax-distr 11099 ax-i2m1 11100 ax-1ne0 11101 ax-1rid 11102 ax-rnegex 11103 ax-rrecex 11104 ax-cnre 11105 ax-pre-lttri 11106 ax-pre-lttrn 11107 ax-pre-ltadd 11108 ax-pre-mulgt0 11109

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 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6260 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-om 7812 df-2nd 7937 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-pnf 11175 df-mnf 11176 df-xr 11177 df-ltxr 11178 df-le 11179 df-sub 11373 df-neg 11374 df-nn 12169 df-2 12238 df-n0 12432 df-z 12519 df-uz 12783 df-seq 13958 df-trcl 14943 df-rtrcl 14944 df-relexp 14976 df-rcl 44121

This theorem is referenced by: cortrclrcl 44191 cotrclrtrcl 44192 cortrclrtrcl 44193

W3C validator