Step | Hyp | Ref
| Expression |
1 | | dfrcl4 36987 |
. 2
⊢ r* =
(𝑎 ∈ V ↦
∪ 𝑖 ∈ {0, 1} (𝑎↑𝑟𝑖)) |
2 | | dftrcl3 37031 |
. 2
⊢ t+ =
(𝑏 ∈ V ↦
∪ 𝑗 ∈ ℕ (𝑏↑𝑟𝑗)) |
3 | | dfrtrcl3 37044 |
. 2
⊢ t* =
(𝑐 ∈ V ↦
∪ 𝑘 ∈ ℕ0 (𝑐↑𝑟𝑘)) |
4 | | prex 4836 |
. 2
⊢ {0, 1}
∈ V |
5 | | nnex 10903 |
. 2
⊢ ℕ
∈ V |
6 | | df-n0 11170 |
. . 3
⊢
ℕ0 = (ℕ ∪ {0}) |
7 | | uncom 3719 |
. . 3
⊢ (ℕ
∪ {0}) = ({0} ∪ ℕ) |
8 | | df-pr 4128 |
. . . . 5
⊢ {0, 1} =
({0} ∪ {1}) |
9 | 8 | uneq1i 3725 |
. . . 4
⊢ ({0, 1}
∪ ℕ) = (({0} ∪ {1}) ∪ ℕ) |
10 | | unass 3732 |
. . . 4
⊢ (({0}
∪ {1}) ∪ ℕ) = ({0} ∪ ({1} ∪ ℕ)) |
11 | | 1nn 10908 |
. . . . . . 7
⊢ 1 ∈
ℕ |
12 | | snssi 4280 |
. . . . . . 7
⊢ (1 ∈
ℕ → {1} ⊆ ℕ) |
13 | 11, 12 | ax-mp 5 |
. . . . . 6
⊢ {1}
⊆ ℕ |
14 | | ssequn1 3745 |
. . . . . 6
⊢ ({1}
⊆ ℕ ↔ ({1} ∪ ℕ) = ℕ) |
15 | 13, 14 | mpbi 219 |
. . . . 5
⊢ ({1}
∪ ℕ) = ℕ |
16 | 15 | uneq2i 3726 |
. . . 4
⊢ ({0}
∪ ({1} ∪ ℕ)) = ({0} ∪ ℕ) |
17 | 9, 10, 16 | 3eqtrri 2637 |
. . 3
⊢ ({0}
∪ ℕ) = ({0, 1} ∪ ℕ) |
18 | 6, 7, 17 | 3eqtri 2636 |
. 2
⊢
ℕ0 = ({0, 1} ∪ ℕ) |
19 | | oveq2 6557 |
. . . 4
⊢ (𝑘 = 𝑖 → (𝑑↑𝑟𝑘) = (𝑑↑𝑟𝑖)) |
20 | 19 | cbviunv 4495 |
. . 3
⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) = ∪ 𝑖 ∈ {0, 1} (𝑑↑𝑟𝑖) |
21 | | ss2iun 4472 |
. . . 4
⊢
(∀𝑖 ∈
{0, 1} (𝑑↑𝑟𝑖) ⊆ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) → ∪
𝑖 ∈ {0, 1} (𝑑↑𝑟𝑖) ⊆ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)) |
22 | | vex 3176 |
. . . . . . . 8
⊢ 𝑑 ∈ V |
23 | | relexp1g 13614 |
. . . . . . . 8
⊢ (𝑑 ∈ V → (𝑑↑𝑟1) =
𝑑) |
24 | 22, 23 | ax-mp 5 |
. . . . . . 7
⊢ (𝑑↑𝑟1) =
𝑑 |
25 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑗 = 1 → (𝑑↑𝑟𝑗) = (𝑑↑𝑟1)) |
26 | 25 | ssiun2s 4500 |
. . . . . . . 8
⊢ (1 ∈
ℕ → (𝑑↑𝑟1) ⊆ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)) |
27 | 11, 26 | ax-mp 5 |
. . . . . . 7
⊢ (𝑑↑𝑟1)
⊆ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) |
28 | 24, 27 | eqsstr3i 3599 |
. . . . . 6
⊢ 𝑑 ⊆ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) |
29 | 28 | a1i 11 |
. . . . 5
⊢ (𝑖 ∈ {0, 1} → 𝑑 ⊆ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)) |
30 | | ovex 6577 |
. . . . . . 7
⊢ (𝑑↑𝑟𝑗) ∈ V |
31 | 5, 30 | iunex 7039 |
. . . . . 6
⊢ ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) ∈ V |
32 | 31 | a1i 11 |
. . . . 5
⊢ (𝑖 ∈ {0, 1} → ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) ∈ V) |
33 | | 0nn0 11184 |
. . . . . . 7
⊢ 0 ∈
ℕ0 |
34 | | 1nn0 11185 |
. . . . . . 7
⊢ 1 ∈
ℕ0 |
35 | | prssi 4293 |
. . . . . . 7
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
⊆ ℕ0) |
36 | 33, 34, 35 | mp2an 704 |
. . . . . 6
⊢ {0, 1}
⊆ ℕ0 |
37 | 36 | sseli 3564 |
. . . . 5
⊢ (𝑖 ∈ {0, 1} → 𝑖 ∈
ℕ0) |
38 | 29, 32, 37 | relexpss1d 37016 |
. . . 4
⊢ (𝑖 ∈ {0, 1} → (𝑑↑𝑟𝑖) ⊆ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)) |
39 | 21, 38 | mprg 2910 |
. . 3
⊢ ∪ 𝑖 ∈ {0, 1} (𝑑↑𝑟𝑖) ⊆ ∪
𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) |
40 | 20, 39 | eqsstri 3598 |
. 2
⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ⊆ ∪
𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) |
41 | | oveq2 6557 |
. . . . 5
⊢ (𝑘 = 𝑗 → (𝑑↑𝑟𝑘) = (𝑑↑𝑟𝑗)) |
42 | 41 | cbviunv 4495 |
. . . 4
⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) = ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) |
43 | | relexp1g 13614 |
. . . . 5
⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) ∈ V → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)) |
44 | 31, 43 | ax-mp 5 |
. . . 4
⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗) |
45 | 42, 44 | eqtr4i 2635 |
. . 3
⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) = (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) |
46 | | 1ex 9914 |
. . . . 5
⊢ 1 ∈
V |
47 | 46 | prid2 4242 |
. . . 4
⊢ 1 ∈
{0, 1} |
48 | | oveq2 6557 |
. . . . 5
⊢ (𝑖 = 1 → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1)) |
49 | 48 | ssiun2s 4500 |
. . . 4
⊢ (1 ∈
{0, 1} → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) ⊆
∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)) |
50 | 47, 49 | ax-mp 5 |
. . 3
⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) ⊆
∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) |
51 | 45, 50 | eqsstri 3598 |
. 2
⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ⊆ ∪
𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) |
52 | | c0ex 9913 |
. . . . . 6
⊢ 0 ∈
V |
53 | 52 | prid1 4241 |
. . . . 5
⊢ 0 ∈
{0, 1} |
54 | | oveq2 6557 |
. . . . . 6
⊢ (𝑘 = 0 → (𝑑↑𝑟𝑘) = (𝑑↑𝑟0)) |
55 | 54 | ssiun2s 4500 |
. . . . 5
⊢ (0 ∈
{0, 1} → (𝑑↑𝑟0) ⊆ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘)) |
56 | 53, 55 | ax-mp 5 |
. . . 4
⊢ (𝑑↑𝑟0)
⊆ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) |
57 | | ssid 3587 |
. . . 4
⊢ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ⊆ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘) |
58 | | unss12 3747 |
. . . 4
⊢ (((𝑑↑𝑟0)
⊆ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∧ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘) ⊆ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) → ((𝑑↑𝑟0) ∪ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) ⊆ (∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∪ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘))) |
59 | 56, 57, 58 | mp2an 704 |
. . 3
⊢ ((𝑑↑𝑟0)
∪ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) ⊆ (∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∪ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
60 | | iuneq1 4470 |
. . . . 5
⊢ ({0, 1} =
({0} ∪ {1}) → ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = ∪ 𝑖 ∈ ({0} ∪ {1})(∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)) |
61 | 8, 60 | ax-mp 5 |
. . . 4
⊢ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = ∪ 𝑖 ∈ ({0} ∪ {1})(∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) |
62 | | iunxun 4541 |
. . . 4
⊢ ∪ 𝑖 ∈ ({0} ∪ {1})(∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑖 ∈ {0} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ∪ ∪
𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)) |
63 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑖 = 0 → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟0)) |
64 | 52, 63 | iunxsn 4539 |
. . . . . 6
⊢ ∪ 𝑖 ∈ {0} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟0) |
65 | | nnssnn0 11172 |
. . . . . . 7
⊢ ℕ
⊆ ℕ0 |
66 | | inelcm 3984 |
. . . . . . . 8
⊢ ((1
∈ {0, 1} ∧ 1 ∈ ℕ) → ({0, 1} ∩ ℕ) ≠
∅) |
67 | 47, 11, 66 | mp2an 704 |
. . . . . . 7
⊢ ({0, 1}
∩ ℕ) ≠ ∅ |
68 | | iunrelexp0 37013 |
. . . . . . 7
⊢ ((𝑑 ∈ V ∧ ℕ ⊆
ℕ0 ∧ ({0, 1} ∩ ℕ) ≠ ∅) → (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟0) = (𝑑↑𝑟0)) |
69 | 22, 65, 67, 68 | mp3an 1416 |
. . . . . 6
⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟0) = (𝑑↑𝑟0) |
70 | 64, 69 | eqtri 2632 |
. . . . 5
⊢ ∪ 𝑖 ∈ {0} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (𝑑↑𝑟0) |
71 | 46, 48 | iunxsn 4539 |
. . . . . 6
⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) |
72 | 44, 42 | eqtr4i 2635 |
. . . . . 6
⊢ (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) |
73 | 71, 72 | eqtri 2632 |
. . . . 5
⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘) |
74 | 70, 73 | uneq12i 3727 |
. . . 4
⊢ (∪ 𝑖 ∈ {0} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ∪ ∪
𝑖 ∈ {1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖)) = ((𝑑↑𝑟0) ∪ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
75 | 61, 62, 74 | 3eqtri 2636 |
. . 3
⊢ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) = ((𝑑↑𝑟0) ∪ ∪ 𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
76 | | iunxun 4541 |
. . 3
⊢ ∪ 𝑘 ∈ ({0, 1} ∪ ℕ)(𝑑↑𝑟𝑘) = (∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∪ ∪
𝑘 ∈ ℕ (𝑑↑𝑟𝑘)) |
77 | 59, 75, 76 | 3sstr4i 3607 |
. 2
⊢ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ ℕ (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈ ({0, 1} ∪
ℕ)(𝑑↑𝑟𝑘) |
78 | 1, 2, 3, 4, 5, 18,
40, 51, 77 | comptiunov2i 37017 |
1
⊢ (r*
∘ t+) = t* |