| Step | Hyp | Ref
| Expression |
| 1 | | iunrelexpmin1.def |
. . . 4
⊢ 𝐶 = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛)) |
| 2 | | simplr 769 |
. . . . 5
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) ∧ 𝑟 = 𝑅) → 𝑁 = ℕ) |
| 3 | | simpr 484 |
. . . . . 6
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅) |
| 4 | 3 | oveq1d 7446 |
. . . . 5
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) ∧ 𝑟 = 𝑅) → (𝑟↑𝑟𝑛) = (𝑅↑𝑟𝑛)) |
| 5 | 2, 4 | iuneq12d 5021 |
. . . 4
⊢ (((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) ∧ 𝑟 = 𝑅) → ∪
𝑛 ∈ 𝑁 (𝑟↑𝑟𝑛) = ∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛)) |
| 6 | | elex 3501 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → 𝑅 ∈ V) |
| 7 | 6 | adantr 480 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) → 𝑅 ∈ V) |
| 8 | | nnex 12272 |
. . . . . 6
⊢ ℕ
∈ V |
| 9 | | ovex 7464 |
. . . . . 6
⊢ (𝑅↑𝑟𝑛) ∈ V |
| 10 | 8, 9 | iunex 7993 |
. . . . 5
⊢ ∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ∈ V |
| 11 | 10 | a1i 11 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) → ∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ∈ V) |
| 12 | 1, 5, 7, 11 | fvmptd2 7024 |
. . 3
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) → (𝐶‘𝑅) = ∪
𝑛 ∈ ℕ (𝑅↑𝑟𝑛)) |
| 13 | | relexp1g 15065 |
. . . . . . . 8
⊢ (𝑅 ∈ 𝑉 → (𝑅↑𝑟1) = 𝑅) |
| 14 | 13 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑅 ∈ 𝑉 → ((𝑅↑𝑟1) ⊆ 𝑠 ↔ 𝑅 ⊆ 𝑠)) |
| 15 | 14 | anbi1d 631 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → (((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) ↔ (𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠))) |
| 16 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → (𝑅↑𝑟𝑥) = (𝑅↑𝑟1)) |
| 17 | 16 | sseq1d 4015 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((𝑅↑𝑟𝑥) ⊆ 𝑠 ↔ (𝑅↑𝑟1) ⊆ 𝑠)) |
| 18 | 17 | imbi2d 340 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟𝑥) ⊆ 𝑠) ↔ ((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟1) ⊆ 𝑠))) |
| 19 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (𝑅↑𝑟𝑥) = (𝑅↑𝑟𝑦)) |
| 20 | 19 | sseq1d 4015 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → ((𝑅↑𝑟𝑥) ⊆ 𝑠 ↔ (𝑅↑𝑟𝑦) ⊆ 𝑠)) |
| 21 | 20 | imbi2d 340 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → (((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟𝑥) ⊆ 𝑠) ↔ ((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟𝑦) ⊆ 𝑠))) |
| 22 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝑦 + 1) → (𝑅↑𝑟𝑥) = (𝑅↑𝑟(𝑦 + 1))) |
| 23 | 22 | sseq1d 4015 |
. . . . . . . . . . . 12
⊢ (𝑥 = (𝑦 + 1) → ((𝑅↑𝑟𝑥) ⊆ 𝑠 ↔ (𝑅↑𝑟(𝑦 + 1)) ⊆ 𝑠)) |
| 24 | 23 | imbi2d 340 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑦 + 1) → (((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟𝑥) ⊆ 𝑠) ↔ ((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟(𝑦 + 1)) ⊆ 𝑠))) |
| 25 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑛 → (𝑅↑𝑟𝑥) = (𝑅↑𝑟𝑛)) |
| 26 | 25 | sseq1d 4015 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑛 → ((𝑅↑𝑟𝑥) ⊆ 𝑠 ↔ (𝑅↑𝑟𝑛) ⊆ 𝑠)) |
| 27 | 26 | imbi2d 340 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑛 → (((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟𝑥) ⊆ 𝑠) ↔ ((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟𝑛) ⊆ 𝑠))) |
| 28 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟1) ⊆ 𝑠) |
| 29 | | simp1 1137 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ (𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) ∧ (𝑅↑𝑟𝑦) ⊆ 𝑠) → 𝑦 ∈ ℕ) |
| 30 | | 1nn 12277 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℕ |
| 31 | 30 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ (𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) ∧ (𝑅↑𝑟𝑦) ⊆ 𝑠) → 1 ∈ ℕ) |
| 32 | | simp2l 1200 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ (𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) ∧ (𝑅↑𝑟𝑦) ⊆ 𝑠) → 𝑅 ∈ 𝑉) |
| 33 | | relexpaddnn 15090 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ 1 ∈
ℕ ∧ 𝑅 ∈
𝑉) → ((𝑅↑𝑟𝑦) ∘ (𝑅↑𝑟1)) = (𝑅↑𝑟(𝑦 + 1))) |
| 34 | 29, 31, 32, 33 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ (𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) ∧ (𝑅↑𝑟𝑦) ⊆ 𝑠) → ((𝑅↑𝑟𝑦) ∘ (𝑅↑𝑟1)) = (𝑅↑𝑟(𝑦 + 1))) |
| 35 | | simp2rr 1244 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ (𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) ∧ (𝑅↑𝑟𝑦) ⊆ 𝑠) → (𝑠 ∘ 𝑠) ⊆ 𝑠) |
| 36 | | simp3 1139 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ (𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) ∧ (𝑅↑𝑟𝑦) ⊆ 𝑠) → (𝑅↑𝑟𝑦) ⊆ 𝑠) |
| 37 | | simp2rl 1243 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℕ ∧ (𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) ∧ (𝑅↑𝑟𝑦) ⊆ 𝑠) → (𝑅↑𝑟1) ⊆ 𝑠) |
| 38 | 35, 36, 37 | trrelssd 15012 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℕ ∧ (𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) ∧ (𝑅↑𝑟𝑦) ⊆ 𝑠) → ((𝑅↑𝑟𝑦) ∘ (𝑅↑𝑟1)) ⊆ 𝑠) |
| 39 | 34, 38 | eqsstrrd 4019 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ ℕ ∧ (𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) ∧ (𝑅↑𝑟𝑦) ⊆ 𝑠) → (𝑅↑𝑟(𝑦 + 1)) ⊆ 𝑠) |
| 40 | 39 | 3exp 1120 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → ((𝑅↑𝑟𝑦) ⊆ 𝑠 → (𝑅↑𝑟(𝑦 + 1)) ⊆ 𝑠))) |
| 41 | 40 | a2d 29 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℕ → (((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟𝑦) ⊆ 𝑠) → ((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟(𝑦 + 1)) ⊆ 𝑠))) |
| 42 | 18, 21, 24, 27, 28, 41 | nnind 12284 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → ((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑅↑𝑟𝑛) ⊆ 𝑠)) |
| 43 | 42 | com12 32 |
. . . . . . . . 9
⊢ ((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → (𝑛 ∈ ℕ → (𝑅↑𝑟𝑛) ⊆ 𝑠)) |
| 44 | 43 | ralrimiv 3145 |
. . . . . . . 8
⊢ ((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → ∀𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ⊆ 𝑠) |
| 45 | | iunss 5045 |
. . . . . . . 8
⊢ (∪ 𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ⊆ 𝑠 ↔ ∀𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ⊆ 𝑠) |
| 46 | 44, 45 | sylibr 234 |
. . . . . . 7
⊢ ((𝑅 ∈ 𝑉 ∧ ((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠)) → ∪
𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ⊆ 𝑠) |
| 47 | 46 | ex 412 |
. . . . . 6
⊢ (𝑅 ∈ 𝑉 → (((𝑅↑𝑟1) ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ∪
𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ⊆ 𝑠)) |
| 48 | 15, 47 | sylbird 260 |
. . . . 5
⊢ (𝑅 ∈ 𝑉 → ((𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ∪
𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ⊆ 𝑠)) |
| 49 | 48 | adantr 480 |
. . . 4
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) → ((𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ∪
𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ⊆ 𝑠)) |
| 50 | | sseq1 4009 |
. . . . 5
⊢ ((𝐶‘𝑅) = ∪
𝑛 ∈ ℕ (𝑅↑𝑟𝑛) → ((𝐶‘𝑅) ⊆ 𝑠 ↔ ∪
𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ⊆ 𝑠)) |
| 51 | 50 | imbi2d 340 |
. . . 4
⊢ ((𝐶‘𝑅) = ∪
𝑛 ∈ ℕ (𝑅↑𝑟𝑛) → (((𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠) ↔ ((𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → ∪
𝑛 ∈ ℕ (𝑅↑𝑟𝑛) ⊆ 𝑠))) |
| 52 | 49, 51 | imbitrrid 246 |
. . 3
⊢ ((𝐶‘𝑅) = ∪
𝑛 ∈ ℕ (𝑅↑𝑟𝑛) → ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) → ((𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠))) |
| 53 | 12, 52 | mpcom 38 |
. 2
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) → ((𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠)) |
| 54 | 53 | alrimiv 1927 |
1
⊢ ((𝑅 ∈ 𝑉 ∧ 𝑁 = ℕ) → ∀𝑠((𝑅 ⊆ 𝑠 ∧ (𝑠 ∘ 𝑠) ⊆ 𝑠) → (𝐶‘𝑅) ⊆ 𝑠)) |