| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | dftrcl3 43738 | . 2
⊢ t+ =
(𝑎 ∈ V ↦
∪ 𝑖 ∈ ℕ (𝑎↑𝑟𝑖)) | 
| 2 |  | dfrcl4 43694 | . 2
⊢ r* =
(𝑏 ∈ V ↦
∪ 𝑗 ∈ {0, 1} (𝑏↑𝑟𝑗)) | 
| 3 |  | dfrtrcl3 43751 | . 2
⊢ t* =
(𝑐 ∈ V ↦
∪ 𝑘 ∈ ℕ0 (𝑐↑𝑟𝑘)) | 
| 4 |  | nnex 12273 | . 2
⊢ ℕ
∈ V | 
| 5 |  | prex 5436 | . 2
⊢ {0, 1}
∈ V | 
| 6 |  | df-n0 12529 | . . 3
⊢
ℕ0 = (ℕ ∪ {0}) | 
| 7 |  | df-pr 4628 | . . . . . 6
⊢ {0, 1} =
({0} ∪ {1}) | 
| 8 | 7 | equncomi 4159 | . . . . 5
⊢ {0, 1} =
({1} ∪ {0}) | 
| 9 | 8 | uneq2i 4164 | . . . 4
⊢ (ℕ
∪ {0, 1}) = (ℕ ∪ ({1} ∪ {0})) | 
| 10 |  | unass 4171 | . . . 4
⊢ ((ℕ
∪ {1}) ∪ {0}) = (ℕ ∪ ({1} ∪ {0})) | 
| 11 |  | 1nn 12278 | . . . . . . 7
⊢ 1 ∈
ℕ | 
| 12 |  | snssi 4807 | . . . . . . 7
⊢ (1 ∈
ℕ → {1} ⊆ ℕ) | 
| 13 | 11, 12 | ax-mp 5 | . . . . . 6
⊢ {1}
⊆ ℕ | 
| 14 |  | ssequn2 4188 | . . . . . 6
⊢ ({1}
⊆ ℕ ↔ (ℕ ∪ {1}) = ℕ) | 
| 15 | 13, 14 | mpbi 230 | . . . . 5
⊢ (ℕ
∪ {1}) = ℕ | 
| 16 | 15 | uneq1i 4163 | . . . 4
⊢ ((ℕ
∪ {1}) ∪ {0}) = (ℕ ∪ {0}) | 
| 17 | 9, 10, 16 | 3eqtr2ri 2771 | . . 3
⊢ (ℕ
∪ {0}) = (ℕ ∪ {0, 1}) | 
| 18 | 6, 17 | eqtri 2764 | . 2
⊢
ℕ0 = (ℕ ∪ {0, 1}) | 
| 19 |  | oveq2 7440 | . . . 4
⊢ (𝑘 = 𝑖 → (𝑑↑𝑟𝑘) = (𝑑↑𝑟𝑖)) | 
| 20 | 19 | cbviunv 5039 | . . 3
⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) = ∪ 𝑖 ∈ ℕ (𝑑↑𝑟𝑖) | 
| 21 |  | ss2iun 5009 | . . . 4
⊢
(∀𝑖 ∈
ℕ (𝑑↑𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) → ∪
𝑖 ∈ ℕ (𝑑↑𝑟𝑖) ⊆ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖)) | 
| 22 |  | 1ex 11258 | . . . . . . . 8
⊢ 1 ∈
V | 
| 23 | 22 | prid2 4762 | . . . . . . 7
⊢ 1 ∈
{0, 1} | 
| 24 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑗 = 1 → (𝑑↑𝑟𝑗) = (𝑑↑𝑟1)) | 
| 25 |  | relexp1g 15066 | . . . . . . . . . 10
⊢ (𝑑 ∈ V → (𝑑↑𝑟1) =
𝑑) | 
| 26 | 25 | elv 3484 | . . . . . . . . 9
⊢ (𝑑↑𝑟1) =
𝑑 | 
| 27 | 24, 26 | eqtrdi 2792 | . . . . . . . 8
⊢ (𝑗 = 1 → (𝑑↑𝑟𝑗) = 𝑑) | 
| 28 | 27 | ssiun2s 5047 | . . . . . . 7
⊢ (1 ∈
{0, 1} → 𝑑 ⊆
∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)) | 
| 29 | 23, 28 | ax-mp 5 | . . . . . 6
⊢ 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) | 
| 30 | 29 | a1i 11 | . . . . 5
⊢ (𝑖 ∈ ℕ → 𝑑 ⊆ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)) | 
| 31 |  | ovex 7465 | . . . . . . 7
⊢ (𝑑↑𝑟𝑗) ∈ V | 
| 32 | 5, 31 | iunex 7994 | . . . . . 6
⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) ∈ V | 
| 33 | 32 | a1i 11 | . . . . 5
⊢ (𝑖 ∈ ℕ → ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) ∈ V) | 
| 34 |  | nnnn0 12535 | . . . . 5
⊢ (𝑖 ∈ ℕ → 𝑖 ∈
ℕ0) | 
| 35 | 30, 33, 34 | relexpss1d 43723 | . . . 4
⊢ (𝑖 ∈ ℕ → (𝑑↑𝑟𝑖) ⊆ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖)) | 
| 36 | 21, 35 | mprg 3066 | . . 3
⊢ ∪ 𝑖 ∈ ℕ (𝑑↑𝑟𝑖) ⊆ ∪
𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) | 
| 37 | 20, 36 | eqsstri 4029 | . 2
⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ⊆ ∪
𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) | 
| 38 |  | oveq2 7440 | . . . . 5
⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟1)) | 
| 39 |  | relexp1g 15066 | . . . . . . 7
⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) ∈ V → (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)) | 
| 40 | 32, 39 | ax-mp 5 | . . . . . 6
⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) | 
| 41 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑑↑𝑟𝑗) = (𝑑↑𝑟𝑘)) | 
| 42 | 41 | cbviunv 5039 | . . . . . 6
⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) = ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) | 
| 43 | 40, 42 | eqtri 2764 | . . . . 5
⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) | 
| 44 | 38, 43 | eqtrdi 2792 | . . . 4
⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘)) | 
| 45 | 44 | ssiun2s 5047 | . . 3
⊢ (1 ∈
ℕ → ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ⊆ ∪
𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖)) | 
| 46 | 11, 45 | ax-mp 5 | . 2
⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ⊆ ∪
𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) | 
| 47 |  | iunss 5044 | . . . 4
⊢ (∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈
ℕ0 (𝑑↑𝑟𝑘) ↔ ∀𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈
ℕ0 (𝑑↑𝑟𝑘)) | 
| 48 |  | iuneq1 5007 | . . . . . . . 8
⊢ ({0, 1} =
({0} ∪ {1}) → ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑𝑟𝑗)) | 
| 49 | 7, 48 | ax-mp 5 | . . . . . . 7
⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) = ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑𝑟𝑗) | 
| 50 |  | iunxun 5093 | . . . . . . 7
⊢ ∪ 𝑗 ∈ ({0} ∪ {1})(𝑑↑𝑟𝑗) = (∪
𝑗 ∈ {0} (𝑑↑𝑟𝑗) ∪ ∪ 𝑗 ∈ {1} (𝑑↑𝑟𝑗)) | 
| 51 |  | c0ex 11256 | . . . . . . . . 9
⊢ 0 ∈
V | 
| 52 |  | oveq2 7440 | . . . . . . . . 9
⊢ (𝑗 = 0 → (𝑑↑𝑟𝑗) = (𝑑↑𝑟0)) | 
| 53 | 51, 52 | iunxsn 5090 | . . . . . . . 8
⊢ ∪ 𝑗 ∈ {0} (𝑑↑𝑟𝑗) = (𝑑↑𝑟0) | 
| 54 | 22, 24 | iunxsn 5090 | . . . . . . . 8
⊢ ∪ 𝑗 ∈ {1} (𝑑↑𝑟𝑗) = (𝑑↑𝑟1) | 
| 55 | 53, 54 | uneq12i 4165 | . . . . . . 7
⊢ (∪ 𝑗 ∈ {0} (𝑑↑𝑟𝑗) ∪ ∪
𝑗 ∈ {1} (𝑑↑𝑟𝑗)) = ((𝑑↑𝑟0) ∪ (𝑑↑𝑟1)) | 
| 56 | 49, 50, 55 | 3eqtri 2768 | . . . . . 6
⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) = ((𝑑↑𝑟0) ∪ (𝑑↑𝑟1)) | 
| 57 | 56 | oveq1i 7442 | . . . . 5
⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑖) | 
| 58 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = 1 → (((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟𝑥) = (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟1)) | 
| 59 | 58 | sseq1d 4014 | . . . . . 6
⊢ (𝑥 = 1 → ((((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟𝑥) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ↔ (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟1)
⊆ ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘))) | 
| 60 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = 𝑦 → (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑥) = (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑦)) | 
| 61 | 60 | sseq1d 4014 | . . . . . 6
⊢ (𝑥 = 𝑦 → ((((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑥) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ↔ (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘))) | 
| 62 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑥) = (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟(𝑦 + 1))) | 
| 63 | 62 | sseq1d 4014 | . . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑥) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ↔ (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈
ℕ0 (𝑑↑𝑟𝑘))) | 
| 64 |  | oveq2 7440 | . . . . . . 7
⊢ (𝑥 = 𝑖 → (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑥) = (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑖)) | 
| 65 | 64 | sseq1d 4014 | . . . . . 6
⊢ (𝑥 = 𝑖 → ((((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑥) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ↔ (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑖) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘))) | 
| 66 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑑↑𝑟0)
∈ V | 
| 67 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑑↑𝑟1)
∈ V | 
| 68 | 66, 67 | unex 7765 | . . . . . . . 8
⊢ ((𝑑↑𝑟0)
∪ (𝑑↑𝑟1)) ∈
V | 
| 69 |  | relexp1g 15066 | . . . . . . . 8
⊢ (((𝑑↑𝑟0)
∪ (𝑑↑𝑟1)) ∈ V →
(((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟1)
= ((𝑑↑𝑟0) ∪
(𝑑↑𝑟1))) | 
| 70 | 68, 69 | ax-mp 5 | . . . . . . 7
⊢ (((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟1)
= ((𝑑↑𝑟0) ∪
(𝑑↑𝑟1)) | 
| 71 |  | 0nn0 12543 | . . . . . . . . 9
⊢ 0 ∈
ℕ0 | 
| 72 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑘 = 0 → (𝑑↑𝑟𝑘) = (𝑑↑𝑟0)) | 
| 73 | 72 | ssiun2s 5047 | . . . . . . . . 9
⊢ (0 ∈
ℕ0 → (𝑑↑𝑟0) ⊆ ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘)) | 
| 74 | 71, 73 | ax-mp 5 | . . . . . . . 8
⊢ (𝑑↑𝑟0)
⊆ ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) | 
| 75 |  | 1nn0 12544 | . . . . . . . . 9
⊢ 1 ∈
ℕ0 | 
| 76 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑘 = 1 → (𝑑↑𝑟𝑘) = (𝑑↑𝑟1)) | 
| 77 | 76 | ssiun2s 5047 | . . . . . . . . 9
⊢ (1 ∈
ℕ0 → (𝑑↑𝑟1) ⊆ ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘)) | 
| 78 | 75, 77 | ax-mp 5 | . . . . . . . 8
⊢ (𝑑↑𝑟1)
⊆ ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) | 
| 79 | 74, 78 | unssi 4190 | . . . . . . 7
⊢ ((𝑑↑𝑟0)
∪ (𝑑↑𝑟1)) ⊆
∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) | 
| 80 | 70, 79 | eqsstri 4029 | . . . . . 6
⊢ (((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟1)
⊆ ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) | 
| 81 |  | simpl 482 | . . . . . . . . 9
⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘)) → 𝑦 ∈ ℕ) | 
| 82 |  | relexpsucnnr 15065 | . . . . . . . . 9
⊢ ((((𝑑↑𝑟0)
∪ (𝑑↑𝑟1)) ∈ V ∧
𝑦 ∈ ℕ) →
(((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟(𝑦 + 1)) = ((((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑦) ∘ ((𝑑↑𝑟0) ∪ (𝑑↑𝑟1)))) | 
| 83 | 68, 81, 82 | sylancr 587 | . . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘)) → (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟(𝑦 + 1)) = ((((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑦) ∘ ((𝑑↑𝑟0) ∪ (𝑑↑𝑟1)))) | 
| 84 |  | coss1 5865 | . . . . . . . . . 10
⊢ ((((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) → ((((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑦) ∘ ((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))) ⊆ (∪ 𝑘 ∈
ℕ0 (𝑑↑𝑟𝑘) ∘ ((𝑑↑𝑟0) ∪ (𝑑↑𝑟1)))) | 
| 85 |  | coundi 6266 | . . . . . . . . . . 11
⊢ (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ ((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))) =
((∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟0)) ∪ (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1))) | 
| 86 |  | relexp0g 15062 | . . . . . . . . . . . . . . . 16
⊢ (𝑑 ∈ V → (𝑑↑𝑟0) = (
I ↾ (dom 𝑑 ∪ ran
𝑑))) | 
| 87 | 86 | elv 3484 | . . . . . . . . . . . . . . 15
⊢ (𝑑↑𝑟0) = (
I ↾ (dom 𝑑 ∪ ran
𝑑)) | 
| 88 | 87 | coeq2i 5870 | . . . . . . . . . . . . . 14
⊢ (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟0)) = (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) | 
| 89 |  | coiun1 43670 | . . . . . . . . . . . . . 14
⊢ (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪
𝑘 ∈
ℕ0 ((𝑑↑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) | 
| 90 |  | coires1 6283 | . . . . . . . . . . . . . . . 16
⊢ ((𝑑↑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) | 
| 91 | 90 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ ((𝑑↑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ((𝑑↑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑))) | 
| 92 | 91 | iuneq2i 5012 | . . . . . . . . . . . . . 14
⊢ ∪ 𝑘 ∈ ℕ0 ((𝑑↑𝑟𝑘) ∘ ( I ↾ (dom 𝑑 ∪ ran 𝑑))) = ∪
𝑘 ∈
ℕ0 ((𝑑↑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) | 
| 93 | 88, 89, 92 | 3eqtri 2768 | . . . . . . . . . . . . 13
⊢ (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟0)) = ∪ 𝑘 ∈ ℕ0 ((𝑑↑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) | 
| 94 |  | ss2iun 5009 | . . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
ℕ0 ((𝑑↑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑𝑟𝑘) → ∪
𝑘 ∈
ℕ0 ((𝑑↑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘)) | 
| 95 |  | resss 6018 | . . . . . . . . . . . . . . 15
⊢ ((𝑑↑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑𝑟𝑘) | 
| 96 | 95 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ0
→ ((𝑑↑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ (𝑑↑𝑟𝑘)) | 
| 97 | 94, 96 | mprg 3066 | . . . . . . . . . . . . 13
⊢ ∪ 𝑘 ∈ ℕ0 ((𝑑↑𝑟𝑘) ↾ (dom 𝑑 ∪ ran 𝑑)) ⊆ ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) | 
| 98 | 93, 97 | eqsstri 4029 | . . . . . . . . . . . 12
⊢ (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟0)) ⊆
∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) | 
| 99 |  | coiun1 43670 | . . . . . . . . . . . . . 14
⊢ (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) = ∪ 𝑘 ∈ ℕ0 ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) | 
| 100 |  | iunss2 5048 | . . . . . . . . . . . . . . 15
⊢
(∀𝑘 ∈
ℕ0 ∃𝑖 ∈ ℕ0 ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆ (𝑑↑𝑟𝑖) → ∪ 𝑘 ∈ ℕ0 ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆
∪ 𝑖 ∈ ℕ0 (𝑑↑𝑟𝑖)) | 
| 101 |  | peano2nn0 12568 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ (𝑘 + 1) ∈
ℕ0) | 
| 102 |  | sbcel1v 3855 | . . . . . . . . . . . . . . . . . . 19
⊢
([(𝑘 + 1) /
𝑖]𝑖 ∈ ℕ0 ↔ (𝑘 + 1) ∈
ℕ0) | 
| 103 | 101, 102 | sylibr 234 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ0
→ [(𝑘 + 1) /
𝑖]𝑖 ∈ ℕ0) | 
| 104 |  | vex 3483 | . . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑑 ∈ V | 
| 105 |  | relexpaddss 43736 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 ∈ ℕ0
∧ 1 ∈ ℕ0 ∧ 𝑑 ∈ V) → ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆ (𝑑↑𝑟(𝑘 + 1))) | 
| 106 | 75, 104, 105 | mp3an23 1454 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ℕ0
→ ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆ (𝑑↑𝑟(𝑘 + 1))) | 
| 107 |  | ovex 7465 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 + 1) ∈ V | 
| 108 |  | csbconstg 3917 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 + 1) ∈ V →
⦋(𝑘 + 1) /
𝑖⦌((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) = ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1))) | 
| 109 | 107, 108 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . 20
⊢
⦋(𝑘 +
1) / 𝑖⦌((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) = ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) | 
| 110 |  | csbov2g 7480 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 + 1) ∈ V →
⦋(𝑘 + 1) /
𝑖⦌(𝑑↑𝑟𝑖) = (𝑑↑𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖)) | 
| 111 |  | csbvarg 4433 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 + 1) ∈ V →
⦋(𝑘 + 1) /
𝑖⦌𝑖 = (𝑘 + 1)) | 
| 112 | 111 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑘 + 1) ∈ V → (𝑑↑𝑟⦋(𝑘 + 1) / 𝑖⦌𝑖) = (𝑑↑𝑟(𝑘 + 1))) | 
| 113 | 110, 112 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑘 + 1) ∈ V →
⦋(𝑘 + 1) /
𝑖⦌(𝑑↑𝑟𝑖) = (𝑑↑𝑟(𝑘 + 1))) | 
| 114 | 107, 113 | ax-mp 5 | . . . . . . . . . . . . . . . . . . . 20
⊢
⦋(𝑘 +
1) / 𝑖⦌(𝑑↑𝑟𝑖) = (𝑑↑𝑟(𝑘 + 1)) | 
| 115 | 106, 109,
114 | 3sstr4g 4036 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ ℕ0
→ ⦋(𝑘 +
1) / 𝑖⦌((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆
⦋(𝑘 + 1) /
𝑖⦌(𝑑↑𝑟𝑖)) | 
| 116 |  | sbcssg 4519 | . . . . . . . . . . . . . . . . . . . 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
⊢ (𝑘 ∈ ℕ0
→ [(𝑘 + 1) /
𝑖]((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆ (𝑑↑𝑟𝑖)) | 
| 119 |  | sbcan 3837 | . . . . . . . . . . . . . . . . . 18
⊢
([(𝑘 + 1) /
𝑖](𝑖 ∈ ℕ0
∧ ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆ (𝑑↑𝑟𝑖)) ↔ ([(𝑘 + 1) / 𝑖]𝑖 ∈ ℕ0 ∧
[(𝑘 + 1) / 𝑖]((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆ (𝑑↑𝑟𝑖))) | 
| 120 | 103, 118,
119 | sylanbrc 583 | . . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ ℕ0
→ [(𝑘 + 1) /
𝑖](𝑖 ∈ ℕ0
∧ ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆ (𝑑↑𝑟𝑖))) | 
| 121 | 120 | spesbcd 3882 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ0
→ ∃𝑖(𝑖 ∈ ℕ0
∧ ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆ (𝑑↑𝑟𝑖))) | 
| 122 |  | df-rex 3070 | . . . . . . . . . . . . . . . 16
⊢
(∃𝑖 ∈
ℕ0 ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆ (𝑑↑𝑟𝑖) ↔ ∃𝑖(𝑖 ∈ ℕ0 ∧ ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆ (𝑑↑𝑟𝑖))) | 
| 123 | 121, 122 | sylibr 234 | . . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℕ0
→ ∃𝑖 ∈
ℕ0 ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆ (𝑑↑𝑟𝑖)) | 
| 124 | 100, 123 | mprg 3066 | . . . . . . . . . . . . . 14
⊢ ∪ 𝑘 ∈ ℕ0 ((𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆
∪ 𝑖 ∈ ℕ0 (𝑑↑𝑟𝑖) | 
| 125 | 99, 124 | eqsstri 4029 | . . . . . . . . . . . . 13
⊢ (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆
∪ 𝑖 ∈ ℕ0 (𝑑↑𝑟𝑖) | 
| 126 |  | oveq2 7440 | . . . . . . . . . . . . . 14
⊢ (𝑖 = 𝑘 → (𝑑↑𝑟𝑖) = (𝑑↑𝑟𝑘)) | 
| 127 | 126 | cbviunv 5039 | . . . . . . . . . . . . 13
⊢ ∪ 𝑖 ∈ ℕ0 (𝑑↑𝑟𝑖) = ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) | 
| 128 | 125, 127 | sseqtri 4031 | . . . . . . . . . . . 12
⊢ (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1)) ⊆
∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) | 
| 129 | 98, 128 | unssi 4190 | . . . . . . . . . . 11
⊢
((∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟0)) ∪ (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ (𝑑↑𝑟1))) ⊆
∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) | 
| 130 | 85, 129 | eqsstri 4029 | . . . . . . . . . 10
⊢ (∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) ∘ ((𝑑↑𝑟0) ∪ (𝑑↑𝑟1)))
⊆ ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) | 
| 131 | 84, 130 | sstrdi 3995 | . . . . . . . . 9
⊢ ((((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) → ((((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑦) ∘ ((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))) ⊆ ∪ 𝑘 ∈
ℕ0 (𝑑↑𝑟𝑘)) | 
| 132 | 131 | adantl 481 | . . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘)) → ((((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟𝑦) ∘ ((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))) ⊆ ∪ 𝑘 ∈
ℕ0 (𝑑↑𝑟𝑘)) | 
| 133 | 83, 132 | eqsstrd 4017 | . . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ (((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘)) → (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈
ℕ0 (𝑑↑𝑟𝑘)) | 
| 134 | 133 | ex 412 | . . . . . 6
⊢ (𝑦 ∈ ℕ → ((((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) → (((𝑑↑𝑟0) ∪ (𝑑↑𝑟1))↑𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈
ℕ0 (𝑑↑𝑟𝑘))) | 
| 135 | 59, 61, 63, 65, 80, 134 | nnind 12285 | . . . . 5
⊢ (𝑖 ∈ ℕ → (((𝑑↑𝑟0)
∪ (𝑑↑𝑟1))↑𝑟𝑖) ⊆ ∪
𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘)) | 
| 136 | 57, 135 | eqsstrid 4021 | . . . 4
⊢ (𝑖 ∈ ℕ → (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈
ℕ0 (𝑑↑𝑟𝑘)) | 
| 137 | 47, 136 | mprgbir 3067 | . . 3
⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈
ℕ0 (𝑑↑𝑟𝑘) | 
| 138 |  | iuneq1 5007 | . . . 4
⊢
(ℕ0 = (ℕ ∪ {0, 1}) → ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑𝑟𝑘)) | 
| 139 | 18, 138 | ax-mp 5 | . . 3
⊢ ∪ 𝑘 ∈ ℕ0 (𝑑↑𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ {0, 1})(𝑑↑𝑟𝑘) | 
| 140 | 137, 139 | sseqtri 4031 | . 2
⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈ (ℕ ∪ {0,
1})(𝑑↑𝑟𝑘) | 
| 141 | 1, 2, 3, 4, 5, 18,
37, 46, 140 | comptiunov2i 43724 | 1
⊢ (t+
∘ r*) = t* |