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 38351
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 38329 . 2 t+ = (𝑎 ∈ V ↦ 𝑖 ∈ ℕ (𝑎𝑟𝑖))
2 dfrcl4 38285 . 2 r* = (𝑏 ∈ V ↦ 𝑗 ∈ {0, 1} (𝑏𝑟𝑗))
3 dfrtrcl3 38342 . 2 t* = (𝑐 ∈ V ↦ 𝑘 ∈ ℕ0 (𝑐𝑟𝑘))
4 nnex 11064 . 2 ℕ ∈ V
5 prex 4939 . 2 {0, 1} ∈ V
6 df-n0 11331 . . 3 0 = (ℕ ∪ {0})
7 df-pr 4213 . . . . . 6 {0, 1} = ({0} ∪ {1})
87equncomi 3792 . . . . 5 {0, 1} = ({1} ∪ {0})
98uneq2i 3797 . . . 4 (ℕ ∪ {0, 1}) = (ℕ ∪ ({1} ∪ {0}))
10 unass 3803 . . . 4 ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ ({1} ∪ {0}))
11 1nn 11069 . . . . . . 7 1 ∈ ℕ
12 snssi 4371 . . . . . . 7 (1 ∈ ℕ → {1} ⊆ ℕ)
1311, 12ax-mp 5 . . . . . 6 {1} ⊆ ℕ
14 ssequn2 3819 . . . . . 6 ({1} ⊆ ℕ ↔ (ℕ ∪ {1}) = ℕ)
1513, 14mpbi 220 . . . . 5 (ℕ ∪ {1}) = ℕ
1615uneq1i 3796 . . . 4 ((ℕ ∪ {1}) ∪ {0}) = (ℕ ∪ {0})
179, 10, 163eqtr2ri 2680 . . 3 (ℕ ∪ {0}) = (ℕ ∪ {0, 1})
186, 17eqtri 2673 . 2 0 = (ℕ ∪ {0, 1})
19 oveq2 6698 . . . 4 (𝑘 = 𝑖 → (𝑑𝑟𝑘) = (𝑑𝑟𝑖))
2019cbviunv 4591 . . 3 𝑘 ∈ ℕ (𝑑𝑟𝑘) = 𝑖 ∈ ℕ (𝑑𝑟𝑖)
21 ss2iun 4568 . . . 4 (∀𝑖 ∈ ℕ (𝑑𝑟𝑖) ⊆ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) → 𝑖 ∈ ℕ (𝑑𝑟𝑖) ⊆ 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖))
22 1ex 10073 . . . . . . . 8 1 ∈ V
2322prid2 4330 . . . . . . 7 1 ∈ {0, 1}
24 oveq2 6698 . . . . . . . . 9 (𝑗 = 1 → (𝑑𝑟𝑗) = (𝑑𝑟1))
25 vex 3234 . . . . . . . . . 10 𝑑 ∈ V
26 relexp1g 13810 . . . . . . . . . 10 (𝑑 ∈ V → (𝑑𝑟1) = 𝑑)
2725, 26ax-mp 5 . . . . . . . . 9 (𝑑𝑟1) = 𝑑
2824, 27syl6eq 2701 . . . . . . . 8 (𝑗 = 1 → (𝑑𝑟𝑗) = 𝑑)
2928ssiun2s 4596 . . . . . . 7 (1 ∈ {0, 1} → 𝑑 𝑗 ∈ {0, 1} (𝑑𝑟𝑗))
3023, 29ax-mp 5 . . . . . 6 𝑑 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)
3130a1i 11 . . . . 5 (𝑖 ∈ ℕ → 𝑑 𝑗 ∈ {0, 1} (𝑑𝑟𝑗))
32 ovex 6718 . . . . . . 7 (𝑑𝑟𝑗) ∈ V
335, 32iunex 7189 . . . . . 6 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) ∈ V
3433a1i 11 . . . . 5 (𝑖 ∈ ℕ → 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) ∈ V)
35 nnnn0 11337 . . . . 5 (𝑖 ∈ ℕ → 𝑖 ∈ ℕ0)
3631, 34, 35relexpss1d 38314 . . . 4 (𝑖 ∈ ℕ → (𝑑𝑟𝑖) ⊆ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖))
3721, 36mprg 2955 . . 3 𝑖 ∈ ℕ (𝑑𝑟𝑖) ⊆ 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖)
3820, 37eqsstri 3668 . 2 𝑘 ∈ ℕ (𝑑𝑟𝑘) ⊆ 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖)
39 oveq2 6698 . . . . 5 (𝑖 = 1 → ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) = ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟1))
40 relexp1g 13810 . . . . . . 7 ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) ∈ V → ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟1) = 𝑗 ∈ {0, 1} (𝑑𝑟𝑗))
4133, 40ax-mp 5 . . . . . 6 ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟1) = 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)
42 oveq2 6698 . . . . . . 7 (𝑗 = 𝑘 → (𝑑𝑟𝑗) = (𝑑𝑟𝑘))
4342cbviunv 4591 . . . . . 6 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) = 𝑘 ∈ {0, 1} (𝑑𝑟𝑘)
4441, 43eqtri 2673 . . . . 5 ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟1) = 𝑘 ∈ {0, 1} (𝑑𝑟𝑘)
4539, 44syl6eq 2701 . . . 4 (𝑖 = 1 → ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) = 𝑘 ∈ {0, 1} (𝑑𝑟𝑘))
4645ssiun2s 4596 . . 3 (1 ∈ ℕ → 𝑘 ∈ {0, 1} (𝑑𝑟𝑘) ⊆ 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖))
4711, 46ax-mp 5 . 2 𝑘 ∈ {0, 1} (𝑑𝑟𝑘) ⊆ 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖)
48 iunss 4593 . . . 4 ( 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ↔ ∀𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
49 iuneq1 4566 . . . . . . . 8 ({0, 1} = ({0} ∪ {1}) → 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) = 𝑗 ∈ ({0} ∪ {1})(𝑑𝑟𝑗))
507, 49ax-mp 5 . . . . . . 7 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) = 𝑗 ∈ ({0} ∪ {1})(𝑑𝑟𝑗)
51 iunxun 4637 . . . . . . 7 𝑗 ∈ ({0} ∪ {1})(𝑑𝑟𝑗) = ( 𝑗 ∈ {0} (𝑑𝑟𝑗) ∪ 𝑗 ∈ {1} (𝑑𝑟𝑗))
52 c0ex 10072 . . . . . . . . 9 0 ∈ V
53 oveq2 6698 . . . . . . . . 9 (𝑗 = 0 → (𝑑𝑟𝑗) = (𝑑𝑟0))
5452, 53iunxsn 4635 . . . . . . . 8 𝑗 ∈ {0} (𝑑𝑟𝑗) = (𝑑𝑟0)
5522, 24iunxsn 4635 . . . . . . . 8 𝑗 ∈ {1} (𝑑𝑟𝑗) = (𝑑𝑟1)
5654, 55uneq12i 3798 . . . . . . 7 ( 𝑗 ∈ {0} (𝑑𝑟𝑗) ∪ 𝑗 ∈ {1} (𝑑𝑟𝑗)) = ((𝑑𝑟0) ∪ (𝑑𝑟1))
5750, 51, 563eqtri 2677 . . . . . 6 𝑗 ∈ {0, 1} (𝑑𝑟𝑗) = ((𝑑𝑟0) ∪ (𝑑𝑟1))
5857oveq1i 6700 . . . . 5 ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) = (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑖)
59 oveq2 6698 . . . . . . 7 (𝑥 = 1 → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) = (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟1))
6059sseq1d 3665 . . . . . 6 (𝑥 = 1 → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ↔ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟1) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)))
61 oveq2 6698 . . . . . . 7 (𝑥 = 𝑦 → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) = (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦))
6261sseq1d 3665 . . . . . 6 (𝑥 = 𝑦 → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ↔ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)))
63 oveq2 6698 . . . . . . 7 (𝑥 = (𝑦 + 1) → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) = (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)))
6463sseq1d 3665 . . . . . 6 (𝑥 = (𝑦 + 1) → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ↔ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)))
65 oveq2 6698 . . . . . . 7 (𝑥 = 𝑖 → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) = (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑖))
6665sseq1d 3665 . . . . . 6 (𝑥 = 𝑖 → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑥) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ↔ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)))
67 ovex 6718 . . . . . . . . 9 (𝑑𝑟0) ∈ V
68 ovex 6718 . . . . . . . . 9 (𝑑𝑟1) ∈ V
6967, 68unex 6998 . . . . . . . 8 ((𝑑𝑟0) ∪ (𝑑𝑟1)) ∈ V
70 relexp1g 13810 . . . . . . . 8 (((𝑑𝑟0) ∪ (𝑑𝑟1)) ∈ V → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟1) = ((𝑑𝑟0) ∪ (𝑑𝑟1)))
7169, 70ax-mp 5 . . . . . . 7 (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟1) = ((𝑑𝑟0) ∪ (𝑑𝑟1))
72 0nn0 11345 . . . . . . . . 9 0 ∈ ℕ0
73 oveq2 6698 . . . . . . . . . 10 (𝑘 = 0 → (𝑑𝑟𝑘) = (𝑑𝑟0))
7473ssiun2s 4596 . . . . . . . . 9 (0 ∈ ℕ0 → (𝑑𝑟0) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
7572, 74ax-mp 5 . . . . . . . 8 (𝑑𝑟0) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
76 1nn0 11346 . . . . . . . . 9 1 ∈ ℕ0
77 oveq2 6698 . . . . . . . . . 10 (𝑘 = 1 → (𝑑𝑟𝑘) = (𝑑𝑟1))
7877ssiun2s 4596 . . . . . . . . 9 (1 ∈ ℕ0 → (𝑑𝑟1) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
7976, 78ax-mp 5 . . . . . . . 8 (𝑑𝑟1) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
8075, 79unssi 3821 . . . . . . 7 ((𝑑𝑟0) ∪ (𝑑𝑟1)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
8171, 80eqsstri 3668 . . . . . 6 (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟1) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
82 simpl 472 . . . . . . . . 9 ((𝑦 ∈ ℕ ∧ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)) → 𝑦 ∈ ℕ)
83 relexpsucnnr 13809 . . . . . . . . 9 ((((𝑑𝑟0) ∪ (𝑑𝑟1)) ∈ V ∧ 𝑦 ∈ ℕ) → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)) = ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))))
8469, 82, 83sylancr 696 . . . . . . . 8 ((𝑦 ∈ ℕ ∧ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)) → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)) = ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))))
85 coss1 5310 . . . . . . . . . 10 ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))) ⊆ ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))))
86 coundi 5674 . . . . . . . . . . 11 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))) = (( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟0)) ∪ ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟1)))
87 relexp0g 13806 . . . . . . . . . . . . . . . 16 (𝑑 ∈ V → (𝑑𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
8825, 87ax-mp 5 . . . . . . . . . . . . . . 15 (𝑑𝑟0) = ( I ↾ (dom 𝑑 ∪ ran 𝑑))
8988coeq2i 5315 . . . . . . . . . . . . . 14 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟0)) = ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
90 coiun1 38261 . . . . . . . . . . . . . 14 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑)))
91 coires1 5691 . . . . . . . . . . . . . . . 16 ((𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
9291a1i 11 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ((𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)))
9392iuneq2i 4571 . . . . . . . . . . . . . 14 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
9489, 90, 933eqtri 2677 . . . . . . . . . . . . 13 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟0)) = 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))
95 ss2iun 4568 . . . . . . . . . . . . . 14 (∀𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑𝑟𝑘) → 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
96 resss 5457 . . . . . . . . . . . . . . 15 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑𝑟𝑘)
9796a1i 11 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑𝑟𝑘))
9895, 97mprg 2955 . . . . . . . . . . . . 13 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
9994, 98eqsstri 3668 . . . . . . . . . . . 12 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟0)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
100 coiun1 38261 . . . . . . . . . . . . . 14 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟1)) = 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1))
101 iunss2 4597 . . . . . . . . . . . . . . 15 (∀𝑘 ∈ ℕ0𝑖 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖) → 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ 𝑖 ∈ ℕ0 (𝑑𝑟𝑖))
102 peano2nn0 11371 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ0 → (𝑘 + 1) ∈ ℕ0)
103 sbcel1v 3528 . . . . . . . . . . . . . . . . . . 19 ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ0 ↔ (𝑘 + 1) ∈ ℕ0)
104102, 103sylibr 224 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0[(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ0)
105 relexpaddss 38327 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 ∈ ℕ0 ∧ 1 ∈ ℕ0𝑑 ∈ V) → ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟(𝑘 + 1)))
10676, 25, 105mp3an23 1456 . . . . . . . . . . . . . . . . . . . 20 (𝑘 ∈ ℕ0 → ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟(𝑘 + 1)))
107 ovex 6718 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 + 1) ∈ V
108 csbconstg 3579 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 + 1) ∈ V → (𝑘 + 1) / 𝑖((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) = ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)))
109107, 108ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑘 + 1) / 𝑖((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) = ((𝑑𝑟𝑘) ∘ (𝑑𝑟1))
110 csbov2g 6731 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 + 1) ∈ V → (𝑘 + 1) / 𝑖(𝑑𝑟𝑖) = (𝑑𝑟(𝑘 + 1) / 𝑖𝑖))
111 csbvarg 4036 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 + 1) ∈ V → (𝑘 + 1) / 𝑖𝑖 = (𝑘 + 1))
112111oveq2d 6706 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑘 + 1) ∈ V → (𝑑𝑟(𝑘 + 1) / 𝑖𝑖) = (𝑑𝑟(𝑘 + 1)))
113110, 112eqtrd 2685 . . . . . . . . . . . . . . . . . . . . 21 ((𝑘 + 1) ∈ V → (𝑘 + 1) / 𝑖(𝑑𝑟𝑖) = (𝑑𝑟(𝑘 + 1)))
114107, 113ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑘 + 1) / 𝑖(𝑑𝑟𝑖) = (𝑑𝑟(𝑘 + 1))
115106, 109, 1143sstr4g 3679 . . . . . . . . . . . . . . . . . . 19 (𝑘 ∈ ℕ0(𝑘 + 1) / 𝑖((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑘 + 1) / 𝑖(𝑑𝑟𝑖))
116 sbcssg 4118 . . . . . . . . . . . . . . . . . . . 20 ((𝑘 + 1) ∈ V → ([(𝑘 + 1) / 𝑖]((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖) ↔ (𝑘 + 1) / 𝑖((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑘 + 1) / 𝑖(𝑑𝑟𝑖)))
117107, 116ax-mp 5 . . . . . . . . . . . . . . . . . . 19 ([(𝑘 + 1) / 𝑖]((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖) ↔ (𝑘 + 1) / 𝑖((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑘 + 1) / 𝑖(𝑑𝑟𝑖))
118115, 117sylibr 224 . . . . . . . . . . . . . . . . . 18 (𝑘 ∈ ℕ0[(𝑘 + 1) / 𝑖]((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖))
119 sbcan 3511 . . . . . . . . . . . . . . . . . 18 ([(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ0 ∧ ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖)) ↔ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ0[(𝑘 + 1) / 𝑖]((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖)))
120104, 118, 119sylanbrc 699 . . . . . . . . . . . . . . . . 17 (𝑘 ∈ ℕ0[(𝑘 + 1) / 𝑖](𝑖 ∈ ℕ0 ∧ ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖)))
121120spesbcd 3555 . . . . . . . . . . . . . . . 16 (𝑘 ∈ ℕ0 → ∃𝑖(𝑖 ∈ ℕ0 ∧ ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖)))
122 df-rex 2947 . . . . . . . . . . . . . . . 16 (∃𝑖 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖) ↔ ∃𝑖(𝑖 ∈ ℕ0 ∧ ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖)))
123121, 122sylibr 224 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ∃𝑖 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ (𝑑𝑟𝑖))
124101, 123mprg 2955 . . . . . . . . . . . . . 14 𝑘 ∈ ℕ0 ((𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ 𝑖 ∈ ℕ0 (𝑑𝑟𝑖)
125100, 124eqsstri 3668 . . . . . . . . . . . . 13 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ 𝑖 ∈ ℕ0 (𝑑𝑟𝑖)
126 oveq2 6698 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (𝑑𝑟𝑖) = (𝑑𝑟𝑘))
127126cbviunv 4591 . . . . . . . . . . . . 13 𝑖 ∈ ℕ0 (𝑑𝑟𝑖) = 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
128125, 127sseqtri 3670 . . . . . . . . . . . 12 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟1)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
12999, 128unssi 3821 . . . . . . . . . . 11 (( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟0)) ∪ ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ (𝑑𝑟1))) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
13086, 129eqsstri 3668 . . . . . . . . . 10 ( 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
13185, 130syl6ss 3648 . . . . . . . . 9 ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
132131adantl 481 . . . . . . . 8 ((𝑦 ∈ ℕ ∧ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)) → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ∘ ((𝑑𝑟0) ∪ (𝑑𝑟1))) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
13384, 132eqsstrd 3672 . . . . . . 7 ((𝑦 ∈ ℕ ∧ (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)) → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
134133ex 449 . . . . . 6 (𝑦 ∈ ℕ → ((((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑦) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟(𝑦 + 1)) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)))
13560, 62, 64, 66, 81, 134nnind 11076 . . . . 5 (𝑖 ∈ ℕ → (((𝑑𝑟0) ∪ (𝑑𝑟1))↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
13658, 135syl5eqss 3682 . . . 4 (𝑖 ∈ ℕ → ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘))
13748, 136mprgbir 2956 . . 3 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) ⊆ 𝑘 ∈ ℕ0 (𝑑𝑟𝑘)
138 iuneq1 4566 . . . 4 (ℕ0 = (ℕ ∪ {0, 1}) → 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) = 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑𝑟𝑘))
13918, 138ax-mp 5 . . 3 𝑘 ∈ ℕ0 (𝑑𝑟𝑘) = 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑𝑟𝑘)
140137, 139sseqtri 3670 . 2 𝑖 ∈ ℕ ( 𝑗 ∈ {0, 1} (𝑑𝑟𝑗)↑𝑟𝑖) ⊆ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑𝑟𝑘)
1411, 2, 3, 4, 5, 18, 38, 47, 140comptiunov2i 38315 1 (t+ ∘ r*) = t*
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1523  wex 1744  wcel 2030  wrex 2942  Vcvv 3231  [wsbc 3468  csb 3566  cun 3605  wss 3607  {csn 4210  {cpr 4212   ciun 4552   I cid 5052  dom cdm 5143  ran crn 5144  cres 5145  ccom 5147  (class class class)co 6690  0cc0 9974  1c1 9975   + caddc 9977  cn 11058  0cn0 11330  t+ctcl 13770  t*crtcl 13771  𝑟crelexp 13804  r*crcl 38281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-seq 12842  df-trcl 13772  df-rtrcl 13773  df-relexp 13805  df-rcl 38282
This theorem is referenced by:  cortrclrcl  38352  cotrclrtrcl  38353  cortrclrtrcl  38354
  Copyright terms: Public domain W3C validator