Step | Hyp | Ref
| Expression |
1 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑅 ∈ V) → 𝑅 ∈ V) |
2 | | nn0ex 12096 |
. . . . . . 7
⊢
ℕ0 ∈ V |
3 | | ovex 7246 |
. . . . . . 7
⊢ (𝑅↑𝑟𝑛) ∈ V |
4 | 2, 3 | iunex 7741 |
. . . . . 6
⊢ ∪ 𝑛 ∈ ℕ0 (𝑅↑𝑟𝑛) ∈ V |
5 | | oveq1 7220 |
. . . . . . . 8
⊢ (𝑟 = 𝑅 → (𝑟↑𝑟𝑛) = (𝑅↑𝑟𝑛)) |
6 | 5 | iuneq2d 4933 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → ∪
𝑛 ∈
ℕ0 (𝑟↑𝑟𝑛) = ∪ 𝑛 ∈ ℕ0
(𝑅↑𝑟𝑛)) |
7 | | eqid 2737 |
. . . . . . 7
⊢ (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) = (𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) |
8 | 6, 7 | fvmptg 6816 |
. . . . . 6
⊢ ((𝑅 ∈ V ∧ ∪ 𝑛 ∈ ℕ0 (𝑅↑𝑟𝑛) ∈ V) → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅) = ∪
𝑛 ∈
ℕ0 (𝑅↑𝑟𝑛)) |
9 | 1, 4, 8 | sylancl 589 |
. . . . 5
⊢ ((𝜑 ∧ 𝑅 ∈ V) → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅) = ∪
𝑛 ∈
ℕ0 (𝑅↑𝑟𝑛)) |
10 | 9 | ex 416 |
. . . 4
⊢ (𝜑 → (𝑅 ∈ V → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅) = ∪
𝑛 ∈
ℕ0 (𝑅↑𝑟𝑛))) |
11 | | iun0 4970 |
. . . . . 6
⊢ ∪ 𝑛 ∈ ℕ0 ∅ =
∅ |
12 | 11 | a1i 11 |
. . . . 5
⊢ (¬
𝑅 ∈ V → ∪ 𝑛 ∈ ℕ0 ∅ =
∅) |
13 | | reldmrelexp 14584 |
. . . . . . 7
⊢ Rel dom
↑𝑟 |
14 | 13 | ovprc1 7252 |
. . . . . 6
⊢ (¬
𝑅 ∈ V → (𝑅↑𝑟𝑛) = ∅) |
15 | 14 | iuneq2d 4933 |
. . . . 5
⊢ (¬
𝑅 ∈ V → ∪ 𝑛 ∈ ℕ0 (𝑅↑𝑟𝑛) = ∪ 𝑛 ∈ ℕ0
∅) |
16 | | fvprc 6709 |
. . . . 5
⊢ (¬
𝑅 ∈ V → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅) = ∅) |
17 | 12, 15, 16 | 3eqtr4rd 2788 |
. . . 4
⊢ (¬
𝑅 ∈ V → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅) = ∪
𝑛 ∈
ℕ0 (𝑅↑𝑟𝑛)) |
18 | 10, 17 | pm2.61d1 183 |
. . 3
⊢ (𝜑 → ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅) = ∪
𝑛 ∈
ℕ0 (𝑅↑𝑟𝑛)) |
19 | | breq 5055 |
. . . 4
⊢ (((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅) = ∪
𝑛 ∈
ℕ0 (𝑅↑𝑟𝑛) → (𝐴((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅)𝐵 ↔ 𝐴∪ 𝑛 ∈ ℕ0
(𝑅↑𝑟𝑛)𝐵)) |
20 | | eliun 4908 |
. . . . . 6
⊢
(〈𝐴, 𝐵〉 ∈ ∪ 𝑛 ∈ ℕ0 (𝑅↑𝑟𝑛) ↔ ∃𝑛 ∈ ℕ0
〈𝐴, 𝐵〉 ∈ (𝑅↑𝑟𝑛)) |
21 | 20 | a1i 11 |
. . . . 5
⊢ (𝜑 → (〈𝐴, 𝐵〉 ∈ ∪ 𝑛 ∈ ℕ0 (𝑅↑𝑟𝑛) ↔ ∃𝑛 ∈ ℕ0
〈𝐴, 𝐵〉 ∈ (𝑅↑𝑟𝑛))) |
22 | | df-br 5054 |
. . . . 5
⊢ (𝐴∪ 𝑛 ∈ ℕ0 (𝑅↑𝑟𝑛)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ ∪ 𝑛 ∈ ℕ0 (𝑅↑𝑟𝑛)) |
23 | | df-br 5054 |
. . . . . 6
⊢ (𝐴(𝑅↑𝑟𝑛)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝑅↑𝑟𝑛)) |
24 | 23 | rexbii 3170 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵 ↔ ∃𝑛 ∈ ℕ0 〈𝐴, 𝐵〉 ∈ (𝑅↑𝑟𝑛)) |
25 | 21, 22, 24 | 3bitr4g 317 |
. . . 4
⊢ (𝜑 → (𝐴∪ 𝑛 ∈ ℕ0
(𝑅↑𝑟𝑛)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵)) |
26 | 19, 25 | sylan9bb 513 |
. . 3
⊢ ((((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅) = ∪
𝑛 ∈
ℕ0 (𝑅↑𝑟𝑛) ∧ 𝜑) → (𝐴((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵)) |
27 | 18, 26 | mpancom 688 |
. 2
⊢ (𝜑 → (𝐴((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵)) |
28 | | df-rtrclrec 14619 |
. . 3
⊢ t*rec =
(𝑟 ∈ V ↦
∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) |
29 | | fveq1 6716 |
. . . . . 6
⊢ (t*rec =
(𝑟 ∈ V ↦
∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) → (t*rec‘𝑅) = ((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅)) |
30 | 29 | breqd 5064 |
. . . . 5
⊢ (t*rec =
(𝑟 ∈ V ↦
∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) → (𝐴(t*rec‘𝑅)𝐵 ↔ 𝐴((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅)𝐵)) |
31 | 30 | bibi1d 347 |
. . . 4
⊢ (t*rec =
(𝑟 ∈ V ↦
∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) → ((𝐴(t*rec‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵) ↔ (𝐴((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵))) |
32 | 31 | imbi2d 344 |
. . 3
⊢ (t*rec =
(𝑟 ∈ V ↦
∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛)) → ((𝜑 → (𝐴(t*rec‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵)) ↔ (𝜑 → (𝐴((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵)))) |
33 | 28, 32 | ax-mp 5 |
. 2
⊢ ((𝜑 → (𝐴(t*rec‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵)) ↔ (𝜑 → (𝐴((𝑟 ∈ V ↦ ∪ 𝑛 ∈ ℕ0 (𝑟↑𝑟𝑛))‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵))) |
34 | 27, 33 | mpbir 234 |
1
⊢ (𝜑 → (𝐴(t*rec‘𝑅)𝐵 ↔ ∃𝑛 ∈ ℕ0 𝐴(𝑅↑𝑟𝑛)𝐵)) |