Step |
Hyp |
Ref |
Expression |
1 |
|
df-rtrcl |
⊢ t* = ( 𝑟 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) |
2 |
|
relexp0g |
⊢ ( 𝑟 ∈ V → ( 𝑟 ↑𝑟 0 ) = ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ) |
3 |
|
nn0ex |
⊢ ℕ0 ∈ V |
4 |
|
0nn0 |
⊢ 0 ∈ ℕ0 |
5 |
|
oveq1 |
⊢ ( 𝑎 = 𝑡 → ( 𝑎 ↑𝑟 𝑛 ) = ( 𝑡 ↑𝑟 𝑛 ) ) |
6 |
5
|
iuneq2d |
⊢ ( 𝑎 = 𝑡 → ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑡 ↑𝑟 𝑛 ) ) |
7 |
|
oveq2 |
⊢ ( 𝑛 = 𝑘 → ( 𝑡 ↑𝑟 𝑛 ) = ( 𝑡 ↑𝑟 𝑘 ) ) |
8 |
7
|
cbviunv |
⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑡 ↑𝑟 𝑛 ) = ∪ 𝑘 ∈ ℕ0 ( 𝑡 ↑𝑟 𝑘 ) |
9 |
6 8
|
eqtrdi |
⊢ ( 𝑎 = 𝑡 → ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) = ∪ 𝑘 ∈ ℕ0 ( 𝑡 ↑𝑟 𝑘 ) ) |
10 |
9
|
cbvmptv |
⊢ ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) = ( 𝑡 ∈ V ↦ ∪ 𝑘 ∈ ℕ0 ( 𝑡 ↑𝑟 𝑘 ) ) |
11 |
10
|
ov2ssiunov2 |
⊢ ( ( 𝑟 ∈ V ∧ ℕ0 ∈ V ∧ 0 ∈ ℕ0 ) → ( 𝑟 ↑𝑟 0 ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
12 |
3 4 11
|
mp3an23 |
⊢ ( 𝑟 ∈ V → ( 𝑟 ↑𝑟 0 ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
13 |
2 12
|
eqsstrrd |
⊢ ( 𝑟 ∈ V → ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
14 |
|
relexp1g |
⊢ ( 𝑟 ∈ V → ( 𝑟 ↑𝑟 1 ) = 𝑟 ) |
15 |
|
1nn0 |
⊢ 1 ∈ ℕ0 |
16 |
10
|
ov2ssiunov2 |
⊢ ( ( 𝑟 ∈ V ∧ ℕ0 ∈ V ∧ 1 ∈ ℕ0 ) → ( 𝑟 ↑𝑟 1 ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
17 |
3 15 16
|
mp3an23 |
⊢ ( 𝑟 ∈ V → ( 𝑟 ↑𝑟 1 ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
18 |
14 17
|
eqsstrrd |
⊢ ( 𝑟 ∈ V → 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
19 |
|
nn0uz |
⊢ ℕ0 = ( ℤ≥ ‘ 0 ) |
20 |
10
|
iunrelexpuztr |
⊢ ( ( 𝑟 ∈ V ∧ ℕ0 = ( ℤ≥ ‘ 0 ) ∧ 0 ∈ ℕ0 ) → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
21 |
19 4 20
|
mp3an23 |
⊢ ( 𝑟 ∈ V → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
22 |
|
fvex |
⊢ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ V |
23 |
|
sseq2 |
⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ↔ ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) |
24 |
|
sseq2 |
⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( 𝑟 ⊆ 𝑧 ↔ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) |
25 |
|
id |
⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
26 |
25 25
|
coeq12d |
⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( 𝑧 ∘ 𝑧 ) = ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) |
27 |
26 25
|
sseq12d |
⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ↔ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) |
28 |
23 24 27
|
3anbi123d |
⊢ ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) |
29 |
28
|
a1i |
⊢ ( 𝑟 ∈ V → ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) ) |
30 |
29
|
alrimiv |
⊢ ( 𝑟 ∈ V → ∀ 𝑧 ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) ) |
31 |
|
elabgt |
⊢ ( ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ V ∧ ∀ 𝑧 ( 𝑧 = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) ) → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) |
32 |
22 30 31
|
sylancr |
⊢ ( 𝑟 ∈ V → ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ 𝑟 ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∧ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∘ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) ) ) |
33 |
13 18 21 32
|
mpbir3and |
⊢ ( 𝑟 ∈ V → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) |
34 |
|
intss1 |
⊢ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
35 |
33 34
|
syl |
⊢ ( 𝑟 ∈ V → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ⊆ ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
36 |
|
vex |
⊢ 𝑠 ∈ V |
37 |
|
sseq2 |
⊢ ( 𝑧 = 𝑠 → ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ↔ ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ) ) |
38 |
|
sseq2 |
⊢ ( 𝑧 = 𝑠 → ( 𝑟 ⊆ 𝑧 ↔ 𝑟 ⊆ 𝑠 ) ) |
39 |
|
id |
⊢ ( 𝑧 = 𝑠 → 𝑧 = 𝑠 ) |
40 |
39 39
|
coeq12d |
⊢ ( 𝑧 = 𝑠 → ( 𝑧 ∘ 𝑧 ) = ( 𝑠 ∘ 𝑠 ) ) |
41 |
40 39
|
sseq12d |
⊢ ( 𝑧 = 𝑠 → ( ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ↔ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) |
42 |
37 38 41
|
3anbi123d |
⊢ ( 𝑧 = 𝑠 → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ∧ 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) ) |
43 |
36 42
|
elab |
⊢ ( 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ∧ 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) ) |
44 |
|
eqid |
⊢ ℕ0 = ℕ0 |
45 |
10
|
iunrelexpmin2 |
⊢ ( ( 𝑟 ∈ V ∧ ℕ0 = ℕ0 ) → ∀ 𝑠 ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ∧ 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) ) |
46 |
44 45
|
mpan2 |
⊢ ( 𝑟 ∈ V → ∀ 𝑠 ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ∧ 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) ) |
47 |
46
|
19.21bi |
⊢ ( 𝑟 ∈ V → ( ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑠 ∧ 𝑟 ⊆ 𝑠 ∧ ( 𝑠 ∘ 𝑠 ) ⊆ 𝑠 ) → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) ) |
48 |
43 47
|
syl5bi |
⊢ ( 𝑟 ∈ V → ( 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) ) |
49 |
48
|
ralrimiv |
⊢ ( 𝑟 ∈ V → ∀ 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) |
50 |
|
ssint |
⊢ ( ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ↔ ∀ 𝑠 ∈ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ 𝑠 ) |
51 |
49 50
|
sylibr |
⊢ ( 𝑟 ∈ V → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ⊆ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) |
52 |
35 51
|
eqssd |
⊢ ( 𝑟 ∈ V → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) ) |
53 |
|
oveq1 |
⊢ ( 𝑎 = 𝑟 → ( 𝑎 ↑𝑟 𝑛 ) = ( 𝑟 ↑𝑟 𝑛 ) ) |
54 |
53
|
iuneq2d |
⊢ ( 𝑎 = 𝑟 → ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) |
55 |
|
eqid |
⊢ ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) = ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) |
56 |
|
ovex |
⊢ ( 𝑟 ↑𝑟 𝑛 ) ∈ V |
57 |
3 56
|
iunex |
⊢ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ∈ V |
58 |
54 55 57
|
fvmpt |
⊢ ( 𝑟 ∈ V → ( ( 𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑎 ↑𝑟 𝑛 ) ) ‘ 𝑟 ) = ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) |
59 |
52 58
|
eqtrd |
⊢ ( 𝑟 ∈ V → ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } = ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) |
60 |
59
|
mpteq2ia |
⊢ ( 𝑟 ∈ V ↦ ∩ { 𝑧 ∣ ( ( I ↾ ( dom 𝑟 ∪ ran 𝑟 ) ) ⊆ 𝑧 ∧ 𝑟 ⊆ 𝑧 ∧ ( 𝑧 ∘ 𝑧 ) ⊆ 𝑧 ) } ) = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) |
61 |
1 60
|
eqtri |
⊢ t* = ( 𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 ( 𝑟 ↑𝑟 𝑛 ) ) |