Step | Hyp | Ref
| Expression |
1 | | dftrcl3 39406 |
. 2
⊢ t+ =
(𝑎 ∈ V ↦
∪ 𝑖 ∈ ℕ (𝑎↑𝑟𝑖)) |
2 | | dftrcl3 39406 |
. 2
⊢ t+ =
(𝑏 ∈ V ↦
∪ 𝑗 ∈ ℕ (𝑏↑𝑟𝑗)) |
3 | | dftrcl3 39406 |
. 2
⊢ t+ =
(𝑐 ∈ V ↦
∪ 𝑘 ∈ ℕ (𝑐↑𝑟𝑘)) |
4 | | nnex 11442 |
. 2
⊢ ℕ
∈ V |
5 | | unidm 4016 |
. . 3
⊢ (ℕ
∪ ℕ) = ℕ |
6 | 5 | eqcomi 2784 |
. 2
⊢ ℕ =
(ℕ ∪ ℕ) |
7 | | 1ex 10431 |
. . . . . 6
⊢ 1 ∈
V |
8 | | oveq2 6982 |
. . . . . 6
⊢ (𝑖 = 1 → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1)) |
9 | 7, 8 | iunxsn 4877 |
. . . . 5
⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) |
10 | | ovex 7006 |
. . . . . . . 8
⊢ (𝑑↑𝑟𝑗) ∈ V |
11 | 4, 10 | iunex 7478 |
. . . . . . 7
⊢ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) ∈ V |
12 | | relexp1g 14240 |
. . . . . . 7
⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) ∈ V → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)) |
13 | 11, 12 | ax-mp 5 |
. . . . . 6
⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) |
14 | | oveq2 6982 |
. . . . . . 7
⊢ (𝑗 = 𝑘 → (𝑑↑𝑟𝑗) = (𝑑↑𝑟𝑘)) |
15 | 14 | cbviunv 4831 |
. . . . . 6
⊢ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) = ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) |
16 | 13, 15 | eqtri 2799 |
. . . . 5
⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) |
17 | 9, 16 | eqtri 2799 |
. . . 4
⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) |
18 | 17 | eqcomi 2784 |
. . 3
⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) = ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) |
19 | | 1nn 11448 |
. . . . 5
⊢ 1 ∈
ℕ |
20 | | snssi 4613 |
. . . . 5
⊢ (1 ∈
ℕ → {1} ⊆ ℕ) |
21 | 19, 20 | ax-mp 5 |
. . . 4
⊢ {1}
⊆ ℕ |
22 | | iunss1 4803 |
. . . 4
⊢ ({1}
⊆ ℕ → ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)) |
23 | 21, 22 | ax-mp 5 |
. . 3
⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) |
24 | 18, 23 | eqsstri 3890 |
. 2
⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ⊆ ∪
𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) |
25 | | iunss 4833 |
. . . 4
⊢ (∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ↔ ∀𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
26 | | oveq2 6982 |
. . . . . 6
⊢ (𝑥 = 1 → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑥) = (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1)) |
27 | 26 | sseq1d 3887 |
. . . . 5
⊢ (𝑥 = 1 → ((∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑥) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ↔ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) ⊆
∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘))) |
28 | | oveq2 6982 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑥) = (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦)) |
29 | 28 | sseq1d 3887 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ↔ (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘))) |
30 | | oveq2 6982 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑥) = (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟(𝑦 + 1))) |
31 | 30 | sseq1d 3887 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → ((∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑥) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ↔ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘))) |
32 | | oveq2 6982 |
. . . . . 6
⊢ (𝑥 = 𝑖 → (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑥) = (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)) |
33 | 32 | sseq1d 3887 |
. . . . 5
⊢ (𝑥 = 𝑖 → ((∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑥) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ↔ (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘))) |
34 | 16 | eqimssi 3914 |
. . . . 5
⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) ⊆
∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) |
35 | | simpl 475 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) → 𝑦 ∈ ℕ) |
36 | | relexpsucnnr 14239 |
. . . . . . . 8
⊢
((∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) ∈ V ∧ 𝑦 ∈ ℕ) → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟(𝑦 + 1)) = ((∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ∘ ∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗))) |
37 | 11, 35, 36 | sylancr 578 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟(𝑦 + 1)) = ((∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ∘ ∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗))) |
38 | | coss1 5573 |
. . . . . . . . 9
⊢
((∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘) → ((∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ∘ ∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)) ⊆ (∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ∘ ∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗))) |
39 | 38 | adantl 474 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℕ ∧ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) → ((∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ∘ ∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)) ⊆ (∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ∘ ∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗))) |
40 | 15 | coeq2i 5578 |
. . . . . . . . 9
⊢ (∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ∘ ∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)) = (∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ∘ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
41 | | trclfvcotrg 14231 |
. . . . . . . . . 10
⊢
((t+‘𝑑)
∘ (t+‘𝑑))
⊆ (t+‘𝑑) |
42 | | vex 3415 |
. . . . . . . . . . . 12
⊢ 𝑑 ∈ V |
43 | | oveq1 6981 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑑 → (𝑐↑𝑟𝑘) = (𝑑↑𝑟𝑘)) |
44 | 43 | iuneq2d 4818 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑑 → ∪
𝑘 ∈ ℕ (𝑐↑𝑟𝑘) = ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
45 | | ovex 7006 |
. . . . . . . . . . . . . 14
⊢ (𝑑↑𝑟𝑘) ∈ V |
46 | 4, 45 | iunex 7478 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ∈ V |
47 | 44, 3, 46 | fvmpt 6593 |
. . . . . . . . . . . 12
⊢ (𝑑 ∈ V → (t+‘𝑑) = ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
48 | 42, 47 | ax-mp 5 |
. . . . . . . . . . 11
⊢
(t+‘𝑑) =
∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) |
49 | 48, 48 | coeq12i 5581 |
. . . . . . . . . 10
⊢
((t+‘𝑑)
∘ (t+‘𝑑)) =
(∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ∘ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
50 | 41, 49, 48 | 3sstr3i 3898 |
. . . . . . . . 9
⊢ (∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ∘ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) |
51 | 40, 50 | eqsstri 3890 |
. . . . . . . 8
⊢ (∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ∘ ∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) |
52 | 39, 51 | syl6ss 3869 |
. . . . . . 7
⊢ ((𝑦 ∈ ℕ ∧ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) → ((∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ∘ ∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
53 | 37, 52 | eqsstrd 3894 |
. . . . . 6
⊢ ((𝑦 ∈ ℕ ∧ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
54 | 53 | ex 405 |
. . . . 5
⊢ (𝑦 ∈ ℕ →
((∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑦) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘) → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟(𝑦 + 1)) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘))) |
55 | 27, 29, 31, 33, 34, 54 | nnind 11455 |
. . . 4
⊢ (𝑖 ∈ ℕ → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
56 | 25, 55 | mprgbir 3100 |
. . 3
⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘) |
57 | | iuneq1 4805 |
. . . 4
⊢ (ℕ
= (ℕ ∪ ℕ) → ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪ ℕ)(𝑑↑𝑟𝑘)) |
58 | 6, 57 | ax-mp 5 |
. . 3
⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) = ∪ 𝑘 ∈ (ℕ ∪
ℕ)(𝑑↑𝑟𝑘) |
59 | 56, 58 | sseqtri 3892 |
. 2
⊢ ∪ 𝑖 ∈ ℕ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈ (ℕ ∪
ℕ)(𝑑↑𝑟𝑘) |
60 | 1, 2, 3, 4, 4, 6, 24, 24, 59 | comptiunov2i 39392 |
1
⊢ (t+
∘ t+) = t+ |