| Step | Hyp | Ref
| Expression |
| 1 | | dfrcl4 43689 |
. 2
⊢ r* =
(𝑎 ∈ V ↦
∪ 𝑖 ∈ {0, 1} (𝑎↑𝑟𝑖)) |
| 2 | | dfrcl4 43689 |
. 2
⊢ r* =
(𝑏 ∈ V ↦
∪ 𝑗 ∈ {0, 1} (𝑏↑𝑟𝑗)) |
| 3 | | dfrcl4 43689 |
. 2
⊢ r* =
(𝑐 ∈ V ↦
∪ 𝑘 ∈ {0, 1} (𝑐↑𝑟𝑘)) |
| 4 | | prex 5437 |
. 2
⊢ {0, 1}
∈ V |
| 5 | | unidm 4157 |
. . 3
⊢ ({0, 1}
∪ {0, 1}) = {0, 1} |
| 6 | 5 | eqcomi 2746 |
. 2
⊢ {0, 1} =
({0, 1} ∪ {0, 1}) |
| 7 | | oveq2 7439 |
. . . . 5
⊢ (𝑘 = 𝑗 → (𝑑↑𝑟𝑘) = (𝑑↑𝑟𝑗)) |
| 8 | 7 | cbviunv 5040 |
. . . 4
⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) = ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) |
| 9 | | 1ex 11257 |
. . . . . . 7
⊢ 1 ∈
V |
| 10 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑖 = 1 → (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟1)) |
| 11 | 9, 10 | iunxsn 5091 |
. . . . . 6
⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟1) |
| 12 | | ovex 7464 |
. . . . . . . 8
⊢ (𝑑↑𝑟𝑗) ∈ V |
| 13 | 4, 12 | iunex 7993 |
. . . . . . 7
⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) ∈ V |
| 14 | | relexp1g 15065 |
. . . . . . 7
⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) ∈ V → (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)) |
| 15 | 13, 14 | ax-mp 5 |
. . . . . 6
⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟1) = ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) |
| 16 | 11, 15 | eqtri 2765 |
. . . . 5
⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) |
| 17 | 16 | eqcomi 2746 |
. . . 4
⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) = ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) |
| 18 | 8, 17 | eqtri 2765 |
. . 3
⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) = ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) |
| 19 | | snsspr2 4815 |
. . . 4
⊢ {1}
⊆ {0, 1} |
| 20 | | iunss1 5006 |
. . . 4
⊢ ({1}
⊆ {0, 1} → ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑖 ∈ {0, 1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖)) |
| 21 | 19, 20 | ax-mp 5 |
. . 3
⊢ ∪ 𝑖 ∈ {1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑖 ∈ {0, 1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) |
| 22 | 18, 21 | eqsstri 4030 |
. 2
⊢ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ⊆ ∪
𝑖 ∈ {0, 1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) |
| 23 | | c0ex 11255 |
. . . . . 6
⊢ 0 ∈
V |
| 24 | 23 | prid1 4762 |
. . . . 5
⊢ 0 ∈
{0, 1} |
| 25 | | oveq2 7439 |
. . . . . 6
⊢ (𝑘 = 0 → (𝑑↑𝑟𝑘) = (𝑑↑𝑟0)) |
| 26 | 25 | ssiun2s 5048 |
. . . . 5
⊢ (0 ∈
{0, 1} → (𝑑↑𝑟0) ⊆ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘)) |
| 27 | 24, 26 | ax-mp 5 |
. . . 4
⊢ (𝑑↑𝑟0)
⊆ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) |
| 28 | | oveq2 7439 |
. . . . . 6
⊢ (𝑗 = 𝑘 → (𝑑↑𝑟𝑗) = (𝑑↑𝑟𝑘)) |
| 29 | 28 | cbviunv 5040 |
. . . . 5
⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) = ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) |
| 30 | 29 | eqimssi 4044 |
. . . 4
⊢ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) ⊆ ∪
𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) |
| 31 | | unss12 4188 |
. . . 4
⊢ (((𝑑↑𝑟0)
⊆ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∧ ∪
𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗) ⊆ ∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘)) → ((𝑑↑𝑟0) ∪ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)) ⊆ (∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∪ ∪
𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘))) |
| 32 | 27, 30, 31 | mp2an 692 |
. . 3
⊢ ((𝑑↑𝑟0)
∪ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)) ⊆ (∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∪ ∪
𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘)) |
| 33 | | df-pr 4629 |
. . . . 5
⊢ {0, 1} =
({0} ∪ {1}) |
| 34 | | iuneq1 5008 |
. . . . 5
⊢ ({0, 1} =
({0} ∪ {1}) → ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = ∪ 𝑖 ∈ ({0} ∪ {1})(∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖)) |
| 35 | 33, 34 | ax-mp 5 |
. . . 4
⊢ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = ∪ 𝑖 ∈ ({0} ∪ {1})(∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) |
| 36 | | iunxun 5094 |
. . . . 5
⊢ ∪ 𝑖 ∈ ({0} ∪ {1})(∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑖 ∈ {0} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) ∪ ∪
𝑖 ∈ {1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖)) |
| 37 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑖 = 0 → (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟0)) |
| 38 | 23, 37 | iunxsn 5091 |
. . . . . . 7
⊢ ∪ 𝑖 ∈ {0} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = (∪
𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟0) |
| 39 | | vex 3484 |
. . . . . . . 8
⊢ 𝑑 ∈ V |
| 40 | | 0nn0 12541 |
. . . . . . . . 9
⊢ 0 ∈
ℕ0 |
| 41 | | 1nn0 12542 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
| 42 | | prssi 4821 |
. . . . . . . . 9
⊢ ((0
∈ ℕ0 ∧ 1 ∈ ℕ0) → {0, 1}
⊆ ℕ0) |
| 43 | 40, 41, 42 | mp2an 692 |
. . . . . . . 8
⊢ {0, 1}
⊆ ℕ0 |
| 44 | 24, 24 | elini 4199 |
. . . . . . . . 9
⊢ 0 ∈
({0, 1} ∩ {0, 1}) |
| 45 | 44 | ne0ii 4344 |
. . . . . . . 8
⊢ ({0, 1}
∩ {0, 1}) ≠ ∅ |
| 46 | | iunrelexp0 43715 |
. . . . . . . 8
⊢ ((𝑑 ∈ V ∧ {0, 1} ⊆
ℕ0 ∧ ({0, 1} ∩ {0, 1}) ≠ ∅) → (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟0) = (𝑑↑𝑟0)) |
| 47 | 39, 43, 45, 46 | mp3an 1463 |
. . . . . . 7
⊢ (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟0) = (𝑑↑𝑟0) |
| 48 | 38, 47 | eqtri 2765 |
. . . . . 6
⊢ ∪ 𝑖 ∈ {0} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = (𝑑↑𝑟0) |
| 49 | 48, 16 | uneq12i 4166 |
. . . . 5
⊢ (∪ 𝑖 ∈ {0} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) ∪ ∪
𝑖 ∈ {1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖)) = ((𝑑↑𝑟0) ∪ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)) |
| 50 | 36, 49 | eqtri 2765 |
. . . 4
⊢ ∪ 𝑖 ∈ ({0} ∪ {1})(∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = ((𝑑↑𝑟0) ∪ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)) |
| 51 | 35, 50 | eqtri 2765 |
. . 3
⊢ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) = ((𝑑↑𝑟0) ∪ ∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)) |
| 52 | | iunxun 5094 |
. . 3
⊢ ∪ 𝑘 ∈ ({0, 1} ∪ {0, 1})(𝑑↑𝑟𝑘) = (∪ 𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘) ∪ ∪
𝑘 ∈ {0, 1} (𝑑↑𝑟𝑘)) |
| 53 | 32, 51, 52 | 3sstr4i 4035 |
. 2
⊢ ∪ 𝑖 ∈ {0, 1} (∪ 𝑗 ∈ {0, 1} (𝑑↑𝑟𝑗)↑𝑟𝑖) ⊆ ∪
𝑘 ∈ ({0, 1} ∪ {0,
1})(𝑑↑𝑟𝑘) |
| 54 | 1, 2, 3, 4, 4, 6, 22, 22, 53 | comptiunov2i 43719 |
1
⊢ (r*
∘ r*) = r* |