Step | Hyp | Ref
| Expression |
1 | | frsuc 8268 |
. . . . . 6
⊢ (𝐵 ∈ ω →
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘suc 𝐵) = ((𝑦 ∈ V ↦ ∪ 𝑦)‘((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵))) |
2 | | fvex 6787 |
. . . . . . 7
⊢
((rec((𝑦 ∈ V
↦ ∪ 𝑦), 𝐴) ↾ ω)‘𝐵) ∈ V |
3 | | unieq 4850 |
. . . . . . . 8
⊢ (𝑎 = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵) →
∪ 𝑎 = ∪ ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) |
4 | | unieq 4850 |
. . . . . . . . 9
⊢ (𝑦 = 𝑎 → ∪ 𝑦 = ∪
𝑎) |
5 | 4 | cbvmptv 5187 |
. . . . . . . 8
⊢ (𝑦 ∈ V ↦ ∪ 𝑦) =
(𝑎 ∈ V ↦ ∪ 𝑎) |
6 | 2 | uniex 7594 |
. . . . . . . 8
⊢ ∪ ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵) ∈
V |
7 | 3, 5, 6 | fvmpt 6875 |
. . . . . . 7
⊢
(((rec((𝑦 ∈ V
↦ ∪ 𝑦), 𝐴) ↾ ω)‘𝐵) ∈ V → ((𝑦 ∈ V ↦ ∪ 𝑦)‘((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) = ∪ ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) |
8 | 2, 7 | ax-mp 5 |
. . . . . 6
⊢ ((𝑦 ∈ V ↦ ∪ 𝑦)‘((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) = ∪ ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵) |
9 | 1, 8 | eqtrdi 2794 |
. . . . 5
⊢ (𝐵 ∈ ω →
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘suc 𝐵) = ∪
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘𝐵)) |
10 | 9 | adantl 482 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) →
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘suc 𝐵) = ∪
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘𝐵)) |
11 | | ituni.u |
. . . . . . 7
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
12 | 11 | itunifval 10172 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝑈‘𝐴) = (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)) |
13 | 12 | fveq1d 6776 |
. . . . 5
⊢ (𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘suc 𝐵)) |
14 | 13 | adantr 481 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘suc 𝐵)) |
15 | 12 | fveq1d 6776 |
. . . . . 6
⊢ (𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) |
16 | 15 | adantr 481 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) |
17 | 16 | unieqd 4853 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ∪ ((𝑈‘𝐴)‘𝐵) = ∪
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘𝐵)) |
18 | 10, 14, 17 | 3eqtr4d 2788 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
19 | | uni0 4869 |
. . . . 5
⊢ ∪ ∅ = ∅ |
20 | 19 | eqcomi 2747 |
. . . 4
⊢ ∅ =
∪ ∅ |
21 | 11 | itunifn 10173 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝑈‘𝐴) Fn ω) |
22 | 21 | fndmd 6538 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → dom (𝑈‘𝐴) = ω) |
23 | 22 | eleq2d 2824 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (suc 𝐵 ∈ dom (𝑈‘𝐴) ↔ suc 𝐵 ∈ ω)) |
24 | | peano2b 7729 |
. . . . . . . 8
⊢ (𝐵 ∈ ω ↔ suc 𝐵 ∈
ω) |
25 | 23, 24 | bitr4di 289 |
. . . . . . 7
⊢ (𝐴 ∈ V → (suc 𝐵 ∈ dom (𝑈‘𝐴) ↔ 𝐵 ∈ ω)) |
26 | 25 | notbid 318 |
. . . . . 6
⊢ (𝐴 ∈ V → (¬ suc
𝐵 ∈ dom (𝑈‘𝐴) ↔ ¬ 𝐵 ∈ ω)) |
27 | 26 | biimpar 478 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ¬
suc 𝐵 ∈ dom (𝑈‘𝐴)) |
28 | | ndmfv 6804 |
. . . . 5
⊢ (¬
suc 𝐵 ∈ dom (𝑈‘𝐴) → ((𝑈‘𝐴)‘suc 𝐵) = ∅) |
29 | 27, 28 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ∅) |
30 | 22 | eleq2d 2824 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (𝐵 ∈ dom (𝑈‘𝐴) ↔ 𝐵 ∈ ω)) |
31 | 30 | notbid 318 |
. . . . . . 7
⊢ (𝐴 ∈ V → (¬ 𝐵 ∈ dom (𝑈‘𝐴) ↔ ¬ 𝐵 ∈ ω)) |
32 | 31 | biimpar 478 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ¬
𝐵 ∈ dom (𝑈‘𝐴)) |
33 | | ndmfv 6804 |
. . . . . 6
⊢ (¬
𝐵 ∈ dom (𝑈‘𝐴) → ((𝑈‘𝐴)‘𝐵) = ∅) |
34 | 32, 33 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘𝐵) = ∅) |
35 | 34 | unieqd 4853 |
. . . 4
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ∪ ((𝑈‘𝐴)‘𝐵) = ∪
∅) |
36 | 20, 29, 35 | 3eqtr4a 2804 |
. . 3
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
37 | 18, 36 | pm2.61dan 810 |
. 2
⊢ (𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
38 | | 0fv 6813 |
. . . . 5
⊢
(∅‘𝐵) =
∅ |
39 | 38 | unieqi 4852 |
. . . 4
⊢ ∪ (∅‘𝐵) = ∪
∅ |
40 | | 0fv 6813 |
. . . 4
⊢
(∅‘suc 𝐵) = ∅ |
41 | 19, 39, 40 | 3eqtr4ri 2777 |
. . 3
⊢
(∅‘suc 𝐵) = ∪
(∅‘𝐵) |
42 | | fvprc 6766 |
. . . 4
⊢ (¬
𝐴 ∈ V → (𝑈‘𝐴) = ∅) |
43 | 42 | fveq1d 6776 |
. . 3
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = (∅‘suc 𝐵)) |
44 | 42 | fveq1d 6776 |
. . . 4
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) = (∅‘𝐵)) |
45 | 44 | unieqd 4853 |
. . 3
⊢ (¬
𝐴 ∈ V → ∪ ((𝑈‘𝐴)‘𝐵) = ∪
(∅‘𝐵)) |
46 | 41, 43, 45 | 3eqtr4a 2804 |
. 2
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
47 | 37, 46 | pm2.61i 182 |
1
⊢ ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵) |