cotrcltrcl - Mathbox for Richard Penner

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

Theorem cotrcltrcl 37036

Description: The transitive closure is idempotent. (Contributed by RP, 16-Jun-2020.)

**Assertion**
Ref	Expression
cotrcltrcl	⊢ (t+ ∘ t+) = t+

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

Step	Hyp	Ref	Expression
1		dftrcl3 37031	. 2 ⊢ t+ = (𝑎 ∈ V ↦ ∪ 𝑖 ∈ ℕ (𝑎↑_𝑟𝑖))
2		dftrcl3 37031	. 2 ⊢ t+ = (𝑏 ∈ V ↦ ∪ 𝑗 ∈ ℕ (𝑏↑_𝑟𝑗))
3		dftrcl3 37031	. 2 ⊢ t+ = (𝑐 ∈ V ↦ ∪ 𝑘 ∈ ℕ (𝑐↑_𝑟𝑘))
4		nnex 10903	. 2 ⊢ ℕ ∈ V
5		unidm 3718	. . 3 ⊢ (ℕ ∪ ℕ) = ℕ
6	5	eqcomi 2619	. 2 ⊢ ℕ = (ℕ ∪ ℕ)
7		1ex 9914	. . . . . 6 ⊢ 1 ∈ V
8		oveq2 6557	. . . . . 6 ⊢ (𝑖 = 1 → (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟1))
9	7, 8	iunxsn 4539	. . . . 5 ⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟1)
10		ovex 6577	. . . . . . . 8 ⊢ (𝑑↑_𝑟𝑗) ∈ V
11	4, 10	iunex 7039	. . . . . . 7 ⊢ ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗) ∈ V
12		relexp1g 13614	. . . . . . 7 ⊢ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗) ∈ V → (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗))
13	11, 12	ax-mp 5	. . . . . 6 ⊢ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)
14		oveq2 6557	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (𝑑↑_𝑟𝑗) = (𝑑↑_𝑟𝑘))
15	14	cbviunv 4495	. . . . . 6 ⊢ ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗) = ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)
16	13, 15	eqtri 2632	. . . . 5 ⊢ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟1) = ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)
17	9, 16	eqtri 2632	. . . 4 ⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖) = ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)
18	17	eqcomi 2619	. . 3 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) = ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
19		1nn 10908	. . . . 5 ⊢ 1 ∈ ℕ
20		snssi 4280	. . . . 5 ⊢ (1 ∈ ℕ → {1} ⊆ ℕ)
21	19, 20	ax-mp 5	. . . 4 ⊢ {1} ⊆ ℕ
22		iunss1 4468	. . . 4 ⊢ ({1} ⊆ ℕ → ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
23	21, 22	ax-mp 5	. . 3 ⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
24	18, 23	eqsstri 3598	. 2 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖)
25		iunss 4497	. . . 4 ⊢ (∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ↔ ∀𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘))
26		oveq2 6557	. . . . . 6 ⊢ (𝑥 = 1 → (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑥) = (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟1))
27	26	sseq1d 3595	. . . . 5 ⊢ (𝑥 = 1 → ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ↔ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)))
28		oveq2 6557	. . . . . 6 ⊢ (𝑥 = 𝑦 → (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑥) = (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦))
29	28	sseq1d 3595	. . . . 5 ⊢ (𝑥 = 𝑦 → ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ↔ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)))
30		oveq2 6557	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑥) = (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟(𝑦 + 1)))
31	30	sseq1d 3595	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ↔ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)))
32		oveq2 6557	. . . . . 6 ⊢ (𝑥 = 𝑖 → (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑥) = (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖))
33	32	sseq1d 3595	. . . . 5 ⊢ (𝑥 = 𝑖 → ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ↔ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)))
34	16	eqimssi 3622	. . . . 5 ⊢ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟1) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)
35		simpl 472	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)) → 𝑦 ∈ ℕ)
36		relexpsucnnr 13613	. . . . . . . 8 ⊢ ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗) ∈ V ∧ 𝑦 ∈ ℕ) → (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟(𝑦 + 1)) = ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ∘ ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)))
37	11, 35, 36	sylancr 694	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ ∧ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)) → (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟(𝑦 + 1)) = ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ∘ ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)))
38		coss1 5199	. . . . . . . . 9 ⊢ ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) → ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ∘ ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)) ⊆ (∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ∘ ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)))
39	38	adantl 481	. . . . . . . 8 ⊢ ((𝑦 ∈ ℕ ∧ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)) → ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ∘ ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)) ⊆ (∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ∘ ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)))
40	15	coeq2i 5204	. . . . . . . . 9 ⊢ (∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ∘ ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)) = (∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ∘ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘))
41		trclfvcotrg 13605	. . . . . . . . . 10 ⊢ ((t+‘𝑑) ∘ (t+‘𝑑)) ⊆ (t+‘𝑑)
42		vex 3176	. . . . . . . . . . . 12 ⊢ 𝑑 ∈ V
43		oveq1 6556	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝑑 → (𝑐↑_𝑟𝑘) = (𝑑↑_𝑟𝑘))
44	43	iuneq2d 4483	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝑑 → ∪ 𝑘 ∈ ℕ (𝑐↑_𝑟𝑘) = ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘))
45		ovex 6577	. . . . . . . . . . . . . 14 ⊢ (𝑑↑_𝑟𝑘) ∈ V
46	4, 45	iunex 7039	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ∈ V
47	44, 3, 46	fvmpt 6191	. . . . . . . . . . . 12 ⊢ (𝑑 ∈ V → (t+‘𝑑) = ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘))
48	42, 47	ax-mp 5	. . . . . . . . . . 11 ⊢ (t+‘𝑑) = ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)
49	48, 48	coeq12i 5207	. . . . . . . . . 10 ⊢ ((t+‘𝑑) ∘ (t+‘𝑑)) = (∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ∘ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘))
50	41, 49, 48	3sstr3i 3606	. . . . . . . . 9 ⊢ (∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ∘ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)
51	40, 50	eqsstri 3598	. . . . . . . 8 ⊢ (∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) ∘ ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)
52	39, 51	syl6ss 3580	. . . . . . 7 ⊢ ((𝑦 ∈ ℕ ∧ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)) → ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ∘ ∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘))
53	37, 52	eqsstrd 3602	. . . . . 6 ⊢ ((𝑦 ∈ ℕ ∧ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)) → (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘))
54	53	ex 449	. . . . 5 ⊢ (𝑦 ∈ ℕ → ((∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) → (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)))
55	27, 29, 31, 33, 34, 54	nnind 10915	. . . 4 ⊢ (𝑖 ∈ ℕ → (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘))
56	25, 55	mprgbir 2911	. . 3 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘)
57		iuneq1 4470	. . . 4 ⊢ (ℕ = (ℕ ∪ ℕ) → ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ ℕ)(𝑑↑_𝑟𝑘))
58	6, 57	ax-mp 5	. . 3 ⊢ ∪ 𝑘 ∈ ℕ (𝑑↑_𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ ℕ)(𝑑↑_𝑟𝑘)
59	56, 58	sseqtri 3600	. 2 ⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑_𝑟𝑗)↑_𝑟𝑖) ⊆ ∪ 𝑘 ∈ (ℕ ∪ ℕ)(𝑑↑_𝑟𝑘)
60	1, 2, 3, 4, 4, 6, 24, 24, 59	comptiunov2i 37017	1 ⊢ (t+ ∘ t+) = t+

Colors of variables: wff setvar class

Syntax hints: ∧ wa 383 = wceq 1475 ∈ wcel 1977 Vcvv 3173 ∪ cun 3538 ⊆ wss 3540 {csn 4125 ∪ ciun 4455 ∘ ccom 5042 ‘cfv 5804 (class class class)co 6549 1c1 9816 + caddc 9818 ℕcn 10897 t+ctcl 13572 ↑_𝑟crelexp 13608

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-er 7629 df-en 7842 df-dom 7843 df-sdom 7844 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-nn 10898 df-2 10956 df-n0 11170 df-z 11255 df-uz 11564 df-seq 12664 df-trcl 13574 df-relexp 13609

This theorem is referenced by: cortrcltrcl 37051 cotrclrtrcl 37055

W3C validator