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

Theorem cotrclrcl 38534
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.
StepHypRef Expression
1 dftrcl3 38512 . 2 t+ = (𝑎 ∈ V ↦ 𝑖 ∈ ℕ (𝑎𝑟𝑖))
2 dfrcl4 38468 . 2 r* = (𝑏 ∈ V ↦ 𝑗 ∈ {0, 1} (𝑏𝑟𝑗))
3 dfrtrcl3 38525 . 2 t* = (𝑐 ∈ V ↦ 𝑘 ∈ ℕ0 (𝑐𝑟𝑘))
4 nnex 11311 . 2 ℕ ∈ V
5 prex 5099 . 2 {0, 1} ∈ V
6 df-n0 11560 . . 3 0 = (ℕ ∪ {0})
7 df-pr 4373 . . . . . 6 {0, 1} = ({0} ∪ {1})
87equncomi 3958 . . . . 5 {0, 1} = ({1} ∪ {0})
98uneq2i 3963 . . . 4 (ℕ ∪ {0, 1}) = (ℕ ∪ ({1} ∪ {0}))
10 unass 3969 . . . 4 ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ ({1} ∪ {0}))
11 1nn 11316 . . . . . . 7 1 ∈ ℕ
12 snssi 4529 . . . . . . 7 (1 ∈ ℕ → {1} ⊆ ℕ)
1311, 12ax-mp 5 . . . . . 6 {1} ⊆ ℕ
14 ssequn2 3985 . . . . . 6 ({1} ⊆ ℕ ↔ (ℕ ∪ {1}) = ℕ)
1513, 14mpbi 221 . . . . 5 (ℕ ∪ {1}) = ℕ
1615uneq1i 3962 . . . 4 ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ {0})
179, 10, 163eqtr2ri 2835 . . 3 (ℕ ∪ {0}) = (ℕ ∪ {0, 1})
186, 17eqtri 2828 . 2 0 = (ℕ ∪ {0, 1})
19 oveq2 6882 . . . 4 (𝑘 = 𝑖 → (𝑑𝑟𝑘) = (𝑑𝑟𝑖))
2019cbviunv 4751 . . 3 𝑘 ∈ ℕ (𝑑𝑟𝑘) = 𝑖 ∈ ℕ (𝑑𝑟𝑖)
21 ss2iun 4728 . . . 4 (∀𝑖 ∈ ℕ (𝑑𝑟𝑖) ⊆ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) → 𝑖 ∈ ℕ (𝑑𝑟𝑖) ⊆ 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖))
22 1ex 10321 . . . . . . . 8 1 ∈ V
2322prid2 4489 . . . . . . 7 1 ∈ {0, 1}
24 oveq2 6882 . . . . . . . . 9 (𝑗 = 1 → (𝑑𝑟𝑗) = (𝑑𝑟1))
25 vex 3394 . . . . . . . . . 10 𝑑 ∈ V
26 relexp1g 13989 . . . . . . . . . 10 (𝑑 ∈ V → (𝑑𝑟1) = 𝑑)
2725, 26ax-mp 5 . . . . . . . . 9 (𝑑𝑟1) = 𝑑
2824, 27syl6eq 2856 . . . . . . . 8 (𝑗 = 1 → (𝑑𝑟𝑗) = 𝑑)
2928ssiun2s 4756 . . . . . . 7 (1 ∈ {0, 1} → 𝑑 𝑗 ∈ {0, 1} (𝑑𝑟𝑗))
3023, 29ax-mp 5 . . . . . 6 𝑑 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)
3130a1i 11 . . . . 5 (𝑖 ∈ ℕ → 𝑑 𝑗 ∈ {0, 1} (𝑑𝑟𝑗))
32 ovex 6906 . . . . . . 7 (𝑑𝑟𝑗) ∈ V
335, 32iunex 7377 . . . . . 6 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) ∈ V
3433a1i 11 . . . . 5 (𝑖 ∈ ℕ → 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) ∈ V)
35 nnnn0 11566 . . . . 5 (𝑖 ∈ ℕ → 𝑖 ∈ ℕ0)
3631, 34, 35relexpss1d 38497 . . . 4 (𝑖 ∈ ℕ → (𝑑𝑟𝑖) ⊆ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖))
3721, 36mprg 3114 . . 3 𝑖 ∈ ℕ (𝑑𝑟𝑖) ⊆ 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖)
3820, 37eqsstri 3832 . 2 𝑘 ∈ ℕ (𝑑𝑟𝑘) ⊆ 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖)
39 oveq2 6882 . . . . 5 (𝑖 = 1 → ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) = ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟1))
40 relexp1g 13989 . . . . . . 7 ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) ∈ V → ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟1) = 𝑗 ∈ {0, 1} (𝑑𝑟𝑗))
4133, 40ax-mp 5 . . . . . 6 ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟1) = 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)
42 oveq2 6882 . . . . . . 7 (𝑗 = 𝑘 → (𝑑𝑟𝑗) = (𝑑𝑟𝑘))
4342cbviunv 4751 . . . . . 6 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) = 𝑘 ∈ {0, 1} (𝑑𝑟𝑘)
4441, 43eqtri 2828 . . . . 5 ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟1) = 𝑘 ∈ {0, 1} (𝑑𝑟𝑘)
4539, 44syl6eq 2856 . . . 4 (𝑖 = 1 → ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) = 𝑘 ∈ {0, 1} (𝑑𝑟𝑘))
4645ssiun2s 4756 . . 3 (1 ∈ ℕ → 𝑘 ∈ {0, 1} (𝑑𝑟𝑘) ⊆ 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖))
4711, 46ax-mp 5 . 2 𝑘 ∈ {0, 1} (𝑑𝑟𝑘) ⊆ 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖)
48 iunss 4753 . . . 4 ( 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ↔ ∀𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
49 iuneq1 4726 . . . . . . . 8 ({0, 1} = ({0} ∪ {1}) → 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) = 𝑗 ∈ ({0} ∪ {1})(𝑑𝑟𝑗))
507, 49ax-mp 5 . . . . . . 7 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) = 𝑗 ∈ ({0} ∪ {1})(𝑑𝑟𝑗)
51 iunxun 4797 . . . . . . 7 𝑗 ∈ ({0} ∪ {1})(𝑑𝑟𝑗) = ( 𝑗 ∈ {0} (𝑑𝑟𝑗) ∪ 𝑗 ∈ {1} (𝑑𝑟𝑗))
52 c0ex 10319 . . . . . . . . 9 0 ∈ V
53 oveq2 6882 . . . . . . . . 9 (𝑗 = 0 → (𝑑𝑟𝑗) = (𝑑𝑟0))
5452, 53iunxsn 4795 . . . . . . . 8 𝑗 ∈ {0} (𝑑𝑟𝑗) = (𝑑𝑟0)
5522, 24iunxsn 4795 . . . . . . . 8 𝑗 ∈ {1} (𝑑𝑟𝑗) = (𝑑𝑟1)
5654, 55uneq12i 3964 . . . . . . 7 ( 𝑗 ∈ {0} (𝑑𝑟𝑗) ∪ 𝑗 ∈ {1} (𝑑𝑟𝑗)) = ((𝑑𝑟0) ∪ (𝑑𝑟1))
5750, 51, 563eqtri 2832 . . . . . 6 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) = ((𝑑𝑟0) ∪ (𝑑𝑟1))
5857oveq1i 6884 . . . . 5 ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) = (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑖)
59 oveq2 6882 . . . . . . 7 (𝑥 = 1 → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) = (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟1))
6059sseq1d 3829 . . . . . 6 (𝑥 = 1 → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ↔ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟1) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)))
61 oveq2 6882 . . . . . . 7 (𝑥 = 𝑦 → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) = (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦))
6261sseq1d 3829 . . . . . 6 (𝑥 = 𝑦 → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ↔ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)))
63 oveq2 6882 . . . . . . 7 (𝑥 = (𝑦 + 1) → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) = (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)))
6463sseq1d 3829 . . . . . 6 (𝑥 = (𝑦 + 1) → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ↔ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)))
65 oveq2 6882 . . . . . . 7 (𝑥 = 𝑖 → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) = (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑖))
6665sseq1d 3829 . . . . . 6 (𝑥 = 𝑖 → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ↔ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)))
67 ovex 6906 . . . . . . . . 9 (𝑑𝑟0) ∈ V
68 ovex 6906 . . . . . . . . 9 (𝑑𝑟1) ∈ V
6967, 68unex 7186 . . . . . . . 8 ((𝑑𝑟0) ∪ (𝑑𝑟1)) ∈ V
70 relexp1g 13989 . . . . . . . 8 (((𝑑𝑟0) ∪ (𝑑𝑟1)) ∈ V → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟1) = ((𝑑𝑟0) ∪ (𝑑𝑟1)))
7169, 70ax-mp 5 . . . . . . 7 (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟1) = ((𝑑𝑟0) ∪ (𝑑𝑟1))
72 0nn0 11574 . . . . . . . . 9 0 ∈ ℕ0
73 oveq2 6882 . . . . . . . . . 10 (𝑘 = 0 → (𝑑𝑟𝑘) = (𝑑𝑟0))
7473ssiun2s 4756 . . . . . . . . 9 (0 ∈ ℕ0 → (𝑑𝑟0) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
7572, 74ax-mp 5 . . . . . . . 8 (𝑑𝑟0) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
76 1nn0 11575 . . . . . . . . 9 1 ∈ ℕ0
77 oveq2 6882 . . . . . . . . . 10 (𝑘 = 1 → (𝑑𝑟𝑘) = (𝑑𝑟1))
7877ssiun2s 4756 . . . . . . . . 9 (1 ∈ ℕ0 → (𝑑𝑟1) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
7976, 78ax-mp 5 . . . . . . . 8 (𝑑𝑟1) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
8075, 79unssi 3987 . . . . . . 7 ((𝑑𝑟0) ∪ (𝑑𝑟1)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
8171, 80eqsstri 3832 . . . . . 6 (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟1) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
82 simpl 470 . . . . . . . . 9 ((𝑦 ∈ ℕ ∧ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)) → 𝑦 ∈ ℕ)
83 relexpsucnnr 13988 . . . . . . . . 9 ((((𝑑𝑟0) ∪ (𝑑𝑟1)) ∈ V ∧ 𝑦 ∈ ℕ) → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)) = ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))))
8469, 82, 83sylancr 577 . . . . . . . 8 ((𝑦 ∈ ℕ ∧ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)) → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)) = ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))))
85 coss1 5479 . . . . . . . . . 10 ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))) ⊆ ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))))
86 coundi 5850 . . . . . . . . . . 11 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))) = (( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟0)) ∪ ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟1)))
87 relexp0g 13985 . . . . . . . . . . . . . . . 16 (𝑑 ∈ V → (𝑑𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
8825, 87ax-mp 5 . . . . . . . . . . . . . . 15 (𝑑𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑))
8988coeq2i 5484 . . . . . . . . . . . . . 14 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟0)) = ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
90 coiun1 38444 . . . . . . . . . . . . . 14 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
91 coires1 5867 . . . . . . . . . . . . . . . 16 ((𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
9291a1i 11 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ((𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)))
9392iuneq2i 4731 . . . . . . . . . . . . . 14 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
9489, 90, 933eqtri 2832 . . . . . . . . . . . . 13 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟0)) = 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
95 ss2iun 4728 . . . . . . . . . . . . . 14 (∀𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑𝑟𝑘) → 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
96 resss 5625 . . . . . . . . . . . . . . 15 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑𝑟𝑘)
9796a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑𝑟𝑘))
9895, 97mprg 3114 . . . . . . . . . . . . 13 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
9994, 98eqsstri 3832 . . . . . . . . . . . 12 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟0)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
100 coiun1 38444 . . . . . . . . . . . . . 14 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟1)) = 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1))
101 iunss2 4757 . . . . . . . . . . . . . . 15 (∀𝑘 ∈ ℕ0𝑖 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖) → 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ 𝑖 ∈ ℕ0 (𝑑𝑟𝑖))
102 peano2nn0 11599 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
103 sbcel1v 3692 . . . . . . . . . . . . . . . . . . 19 ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ0 ↔ (𝑘 + 1) ∈ ℕ0)
104102, 103sylibr 225 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0[(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ0)
105 relexpaddss 38510 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0 ∧ 1 ∈ ℕ0𝑑 ∈ V) → ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟(𝑘 + 1)))
10676, 25, 105mp3an23 1570 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ0 → ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟(𝑘 + 1)))
107 ovex 6906 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 + 1) ∈ V
108 csbconstg 3741 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 + 1) ∈ V → (𝑘 + 1) / 𝑖((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) = ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)))
109107, 108ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑘 + 1) / 𝑖((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) = ((𝑑𝑟𝑘) ∘ (𝑑𝑟1))
110 csbov2g 6919 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 + 1) ∈ V → (𝑘 + 1) / 𝑖(𝑑𝑟𝑖) = (𝑑𝑟(𝑘 + 1) / 𝑖𝑖))
111 csbvarg 4200 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 + 1) ∈ V → (𝑘 + 1) / 𝑖𝑖 = (𝑘 + 1))
112111oveq2d 6890 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 + 1) ∈ V → (𝑑𝑟(𝑘 + 1) / 𝑖𝑖) = (𝑑𝑟(𝑘 + 1)))
113110, 112eqtrd 2840 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 + 1) ∈ V → (𝑘 + 1) / 𝑖(𝑑𝑟𝑖) = (𝑑𝑟(𝑘 + 1)))
114107, 113ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑘 + 1) / 𝑖(𝑑𝑟𝑖) = (𝑑𝑟(𝑘 + 1))
115106, 109, 1143sstr4g 3843 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ0(𝑘 + 1) / 𝑖((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑘 + 1) / 𝑖(𝑑𝑟𝑖))
116 sbcssg 4278 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 + 1) ∈ V → ([(𝑘 + 1) / 𝑖]((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖) ↔ (𝑘 + 1) / 𝑖((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑘 + 1) / 𝑖(𝑑𝑟𝑖)))
117107, 116ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([(𝑘 + 1) / 𝑖]((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖) ↔ (𝑘 + 1) / 𝑖((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑘 + 1) / 𝑖(𝑑𝑟𝑖))
118115, 117sylibr 225 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0[(𝑘 + 1) / 𝑖]((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖))
119 sbcan 3676 . . . . . . . . . . . . . . . . . 18 ([(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ0 ∧ ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖)) ↔ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ0[(𝑘 + 1) / 𝑖]((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖)))
120104, 118, 119sylanbrc 574 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ0[(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ0 ∧ ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖)))
121120spesbcd 3717 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → ∃𝑖(𝑖 ∈ ℕ0 ∧ ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖)))
122 df-rex 3102 . . . . . . . . . . . . . . . 16 (∃𝑖 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖) ↔ ∃𝑖(𝑖 ∈ ℕ0 ∧ ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖)))
123121, 122sylibr 225 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ∃𝑖 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖))
124101, 123mprg 3114 . . . . . . . . . . . . . 14 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ 𝑖 ∈ ℕ0 (𝑑𝑟𝑖)
125100, 124eqsstri 3832 . . . . . . . . . . . . 13 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ 𝑖 ∈ ℕ0 (𝑑𝑟𝑖)
126 oveq2 6882 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝑑𝑟𝑖) = (𝑑𝑟𝑘))
127126cbviunv 4751 . . . . . . . . . . . . 13 𝑖 ∈ ℕ0 (𝑑𝑟𝑖) = 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
128125, 127sseqtri 3834 . . . . . . . . . . . 12 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
12999, 128unssi 3987 . . . . . . . . . . 11 (( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟0)) ∪ ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟1))) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
13086, 129eqsstri 3832 . . . . . . . . . 10 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
13185, 130syl6ss 3810 . . . . . . . . 9 ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
132131adantl 469 . . . . . . . 8 ((𝑦 ∈ ℕ ∧ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)) → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
13384, 132eqsstrd 3836 . . . . . . 7 ((𝑦 ∈ ℕ ∧ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)) → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
134133ex 399 . . . . . 6 (𝑦 ∈ ℕ → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)))
13560, 62, 64, 66, 81, 134nnind 11323 . . . . 5 (𝑖 ∈ ℕ → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
13658, 135syl5eqss 3846 . . . 4 (𝑖 ∈ ℕ → ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
13748, 136mprgbir 3115 . . 3 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
138 iuneq1 4726 . . . 4 (ℕ0 = (ℕ ∪ {0, 1}) → 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) = 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑𝑟𝑘))
13918, 138ax-mp 5 . . 3 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) = 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑𝑟𝑘)
140137, 139sseqtri 3834 . 2 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) ⊆ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑𝑟𝑘)
1411, 2, 3, 4, 5, 18, 38, 47, 140comptiunov2i 38498 1 (t+ ∘ r*) = t*
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1637  wex 1859  wcel 2156  wrex 3097  Vcvv 3391  [wsbc 3633  csb 3728  cun 3767  wss 3769  {csn 4370  {cpr 4372   ciun 4712   I cid 5218  dom cdm 5311  ran crn 5312  cres 5313  ccom 5315  (class class class)co 6874  0cc0 10221  1c1 10222   + caddc 10224  cn 11305  0cn0 11559  t+ctcl 13949  t*crtcl 13950  𝑟crelexp 13983  r*crcl 38464
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7179  ax-cnex 10277  ax-resscn 10278  ax-1cn 10279  ax-icn 10280  ax-addcl 10281  ax-addrcl 10282  ax-mulcl 10283  ax-mulrcl 10284  ax-mulcom 10285  ax-addass 10286  ax-mulass 10287  ax-distr 10288  ax-i2m1 10289  ax-1ne0 10290  ax-1rid 10291  ax-rnegex 10292  ax-rrecex 10293  ax-cnre 10294  ax-pre-lttri 10295  ax-pre-lttrn 10296  ax-pre-ltadd 10297  ax-pre-mulgt0 10298
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-f1 6106  df-fo 6107  df-f1o 6108  df-fv 6109  df-riota 6835  df-ov 6877  df-oprab 6878  df-mpt2 6879  df-om 7296  df-2nd 7399  df-wrecs 7642  df-recs 7704  df-rdg 7742  df-er 7979  df-en 8193  df-dom 8194  df-sdom 8195  df-pnf 10361  df-mnf 10362  df-xr 10363  df-ltxr 10364  df-le 10365  df-sub 10553  df-neg 10554  df-nn 11306  df-2 11364  df-n0 11560  df-z 11644  df-uz 11905  df-seq 13025  df-trcl 13951  df-rtrcl 13952  df-relexp 13984  df-rcl 38465
This theorem is referenced by:  cortrclrcl  38535  cotrclrtrcl  38536  cortrclrtrcl  38537
  Copyright terms: Public domain W3C validator