Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
⊢ ( 𝑅 ∈ 𝑉 → 𝑅 ∈ V ) |
2 |
|
relexpsucnnr |
⊢ ( ( 𝑅 ∈ V ∧ 𝑛 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( ( 𝑅 ↑𝑟 𝑛 ) ∘ 𝑅 ) ) |
3 |
|
relexpsucnnl |
⊢ ( ( 𝑅 ∈ V ∧ 𝑛 ∈ ℕ ) → ( 𝑅 ↑𝑟 ( 𝑛 + 1 ) ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ) |
4 |
2 3
|
eqtr3d |
⊢ ( ( 𝑅 ∈ V ∧ 𝑛 ∈ ℕ ) → ( ( 𝑅 ↑𝑟 𝑛 ) ∘ 𝑅 ) = ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ) |
5 |
4
|
iuneq2dv |
⊢ ( 𝑅 ∈ V → ∪ 𝑛 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑛 ) ∘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ) |
6 |
|
oveq1 |
⊢ ( 𝑟 = 𝑅 → ( 𝑟 ↑𝑟 𝑛 ) = ( 𝑅 ↑𝑟 𝑛 ) ) |
7 |
6
|
iuneq2d |
⊢ ( 𝑟 = 𝑅 → ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ) |
8 |
|
dftrcl3 |
⊢ t+ = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ ( 𝑟 ↑𝑟 𝑛 ) ) |
9 |
|
nnex |
⊢ ℕ ∈ V |
10 |
|
ovex |
⊢ ( 𝑅 ↑𝑟 𝑛 ) ∈ V |
11 |
9 10
|
iunex |
⊢ ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ∈ V |
12 |
7 8 11
|
fvmpt |
⊢ ( 𝑅 ∈ V → ( t+ ‘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ) |
13 |
12
|
coeq1d |
⊢ ( 𝑅 ∈ V → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = ( ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ∘ 𝑅 ) ) |
14 |
|
coiun1 |
⊢ ( ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ∘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑛 ) ∘ 𝑅 ) |
15 |
13 14
|
eqtrdi |
⊢ ( 𝑅 ∈ V → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = ∪ 𝑛 ∈ ℕ ( ( 𝑅 ↑𝑟 𝑛 ) ∘ 𝑅 ) ) |
16 |
12
|
coeq2d |
⊢ ( 𝑅 ∈ V → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) = ( 𝑅 ∘ ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ) ) |
17 |
|
coiun |
⊢ ( 𝑅 ∘ ∪ 𝑛 ∈ ℕ ( 𝑅 ↑𝑟 𝑛 ) ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) |
18 |
16 17
|
eqtrdi |
⊢ ( 𝑅 ∈ V → ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) = ∪ 𝑛 ∈ ℕ ( 𝑅 ∘ ( 𝑅 ↑𝑟 𝑛 ) ) ) |
19 |
5 15 18
|
3eqtr4d |
⊢ ( 𝑅 ∈ V → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ) |
20 |
1 19
|
syl |
⊢ ( 𝑅 ∈ 𝑉 → ( ( t+ ‘ 𝑅 ) ∘ 𝑅 ) = ( 𝑅 ∘ ( t+ ‘ 𝑅 ) ) ) |