Step | Hyp | Ref
| Expression |
1 | | df-trcl 14449 |
. 2
⊢ t+ =
(𝑟 ∈ V ↦ ∩ {𝑧
∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
2 | | relexp1g 14488 |
. . . . . . . 8
⊢ (𝑟 ∈ V → (𝑟↑𝑟1) =
𝑟) |
3 | | nnex 11735 |
. . . . . . . . 9
⊢ ℕ
∈ V |
4 | | 1nn 11740 |
. . . . . . . . 9
⊢ 1 ∈
ℕ |
5 | | oveq1 7190 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑡 → (𝑎↑𝑟𝑛) = (𝑡↑𝑟𝑛)) |
6 | 5 | iuneq2d 4920 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑡 → ∪
𝑛 ∈ ℕ (𝑎↑𝑟𝑛) = ∪ 𝑛 ∈ ℕ (𝑡↑𝑟𝑛)) |
7 | | oveq2 7191 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝑡↑𝑟𝑛) = (𝑡↑𝑟𝑘)) |
8 | 7 | cbviunv 4936 |
. . . . . . . . . . . 12
⊢ ∪ 𝑛 ∈ ℕ (𝑡↑𝑟𝑛) = ∪ 𝑘 ∈ ℕ (𝑡↑𝑟𝑘) |
9 | 6, 8 | eqtrdi 2790 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑡 → ∪
𝑛 ∈ ℕ (𝑎↑𝑟𝑛) = ∪ 𝑘 ∈ ℕ (𝑡↑𝑟𝑘)) |
10 | 9 | cbvmptv 5143 |
. . . . . . . . . 10
⊢ (𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛)) = (𝑡 ∈ V ↦ ∪ 𝑘 ∈ ℕ (𝑡↑𝑟𝑘)) |
11 | 10 | ov2ssiunov2 40895 |
. . . . . . . . 9
⊢ ((𝑟 ∈ V ∧ ℕ ∈ V
∧ 1 ∈ ℕ) → (𝑟↑𝑟1) ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) |
12 | 3, 4, 11 | mp3an23 1454 |
. . . . . . . 8
⊢ (𝑟 ∈ V → (𝑟↑𝑟1)
⊆ ((𝑎 ∈ V
↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) |
13 | 2, 12 | eqsstrrd 3926 |
. . . . . . 7
⊢ (𝑟 ∈ V → 𝑟 ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) |
14 | | nnuz 12376 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
15 | | 1nn0 12005 |
. . . . . . . 8
⊢ 1 ∈
ℕ0 |
16 | 10 | iunrelexpuztr 40914 |
. . . . . . . 8
⊢ ((𝑟 ∈ V ∧ ℕ =
(ℤ≥‘1) ∧ 1 ∈ ℕ0) →
(((𝑎 ∈ V ↦
∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∘ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) |
17 | 14, 15, 16 | mp3an23 1454 |
. . . . . . 7
⊢ (𝑟 ∈ V → (((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∘ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) |
18 | | fvex 6700 |
. . . . . . . 8
⊢ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∈ V |
19 | | trcleq2lem 14453 |
. . . . . . . . . 10
⊢ (𝑧 = ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) → ((𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ (𝑟 ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∧ (((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∘ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)))) |
20 | 19 | a1i 11 |
. . . . . . . . 9
⊢ (𝑟 ∈ V → (𝑧 = ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) → ((𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ (𝑟 ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∧ (((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∘ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟))))) |
21 | 20 | alrimiv 1934 |
. . . . . . . 8
⊢ (𝑟 ∈ V → ∀𝑧(𝑧 = ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) → ((𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ (𝑟 ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∧ (((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∘ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟))))) |
22 | | elabgt 3572 |
. . . . . . . 8
⊢ ((((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∈ V ∧ ∀𝑧(𝑧 = ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) → ((𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ (𝑟 ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∧ (((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∘ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟))))) → (((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∈ {𝑧 ∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ↔ (𝑟 ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∧ (((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∘ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)))) |
23 | 18, 21, 22 | sylancr 590 |
. . . . . . 7
⊢ (𝑟 ∈ V → (((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∈ {𝑧 ∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ↔ (𝑟 ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∧ (((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∘ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)))) |
24 | 13, 17, 23 | mpbir2and 713 |
. . . . . 6
⊢ (𝑟 ∈ V → ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∈ {𝑧 ∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
25 | | intss1 4861 |
. . . . . 6
⊢ (((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ∈ {𝑧 ∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → ∩ {𝑧 ∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ (𝑟 ∈ V → ∩ {𝑧
∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ⊆ ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) |
27 | | vex 3404 |
. . . . . . . . 9
⊢ 𝑠 ∈ V |
28 | | trcleq2lem 14453 |
. . . . . . . . 9
⊢ (𝑧 = 𝑠 → ((𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧) ↔ (𝑟 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠))) |
29 | 27, 28 | elab 3578 |
. . . . . . . 8
⊢ (𝑠 ∈ {𝑧 ∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ↔ (𝑟 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) |
30 | | eqid 2739 |
. . . . . . . . . 10
⊢ ℕ =
ℕ |
31 | 10 | iunrelexpmin1 40903 |
. . . . . . . . . 10
⊢ ((𝑟 ∈ V ∧ ℕ =
ℕ) → ∀𝑠((𝑟 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ⊆ 𝑠)) |
32 | 30, 31 | mpan2 691 |
. . . . . . . . 9
⊢ (𝑟 ∈ V → ∀𝑠((𝑟 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ⊆ 𝑠)) |
33 | 32 | 19.21bi 2190 |
. . . . . . . 8
⊢ (𝑟 ∈ V → ((𝑟 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ⊆ 𝑠)) |
34 | 29, 33 | syl5bi 245 |
. . . . . . 7
⊢ (𝑟 ∈ V → (𝑠 ∈ {𝑧 ∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} → ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ⊆ 𝑠)) |
35 | 34 | ralrimiv 3096 |
. . . . . 6
⊢ (𝑟 ∈ V → ∀𝑠 ∈ {𝑧 ∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ⊆ 𝑠) |
36 | | ssint 4862 |
. . . . . 6
⊢ (((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ⊆ ∩ {𝑧 ∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ↔ ∀𝑠 ∈ {𝑧 ∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ⊆ 𝑠) |
37 | 35, 36 | sylibr 237 |
. . . . 5
⊢ (𝑟 ∈ V → ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) ⊆ ∩ {𝑧 ∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) |
38 | 26, 37 | eqssd 3904 |
. . . 4
⊢ (𝑟 ∈ V → ∩ {𝑧
∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟)) |
39 | | oveq1 7190 |
. . . . . 6
⊢ (𝑎 = 𝑟 → (𝑎↑𝑟𝑛) = (𝑟↑𝑟𝑛)) |
40 | 39 | iuneq2d 4920 |
. . . . 5
⊢ (𝑎 = 𝑟 → ∪
𝑛 ∈ ℕ (𝑎↑𝑟𝑛) = ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) |
41 | | eqid 2739 |
. . . . 5
⊢ (𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛)) = (𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛)) |
42 | | ovex 7216 |
. . . . . 6
⊢ (𝑟↑𝑟𝑛) ∈ V |
43 | 3, 42 | iunex 7707 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛) ∈ V |
44 | 40, 41, 43 | fvmpt 6788 |
. . . 4
⊢ (𝑟 ∈ V → ((𝑎 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑎↑𝑟𝑛))‘𝑟) = ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) |
45 | 38, 44 | eqtrd 2774 |
. . 3
⊢ (𝑟 ∈ V → ∩ {𝑧
∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)} = ∪
𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) |
46 | 45 | mpteq2ia 5131 |
. 2
⊢ (𝑟 ∈ V ↦ ∩ {𝑧
∣ (𝑟 ⊆ 𝑧 ∧ (𝑧 ∘ 𝑧) ⊆ 𝑧)}) = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) |
47 | 1, 46 | eqtri 2762 |
1
⊢ t+ =
(𝑟 ∈ V ↦
∪ 𝑛 ∈ ℕ (𝑟↑𝑟𝑛)) |