Step | Hyp | Ref
| Expression |
1 | | frsuc 7874 |
. . . . . 6
⊢ (𝐵 ∈ ω →
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘suc 𝐵) = ((𝑦 ∈ V ↦ ∪ 𝑦)‘((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵))) |
2 | | fvex 6509 |
. . . . . . 7
⊢
((rec((𝑦 ∈ V
↦ ∪ 𝑦), 𝐴) ↾ ω)‘𝐵) ∈ V |
3 | | unieq 4716 |
. . . . . . . 8
⊢ (𝑎 = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵) →
∪ 𝑎 = ∪ ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) |
4 | | unieq 4716 |
. . . . . . . . 9
⊢ (𝑦 = 𝑎 → ∪ 𝑦 = ∪
𝑎) |
5 | 4 | cbvmptv 5024 |
. . . . . . . 8
⊢ (𝑦 ∈ V ↦ ∪ 𝑦) =
(𝑎 ∈ V ↦ ∪ 𝑎) |
6 | 2 | uniex 7281 |
. . . . . . . 8
⊢ ∪ ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵) ∈
V |
7 | 3, 5, 6 | fvmpt 6593 |
. . . . . . 7
⊢
(((rec((𝑦 ∈ V
↦ ∪ 𝑦), 𝐴) ↾ ω)‘𝐵) ∈ V → ((𝑦 ∈ V ↦ ∪ 𝑦)‘((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) = ∪ ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) |
8 | 2, 7 | ax-mp 5 |
. . . . . 6
⊢ ((𝑦 ∈ V ↦ ∪ 𝑦)‘((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) = ∪ ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵) |
9 | 1, 8 | syl6eq 2823 |
. . . . 5
⊢ (𝐵 ∈ ω →
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘suc 𝐵) = ∪
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘𝐵)) |
10 | 9 | adantl 474 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) →
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘suc 𝐵) = ∪
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘𝐵)) |
11 | | ituni.u |
. . . . . . 7
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
12 | 11 | itunifval 9634 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝑈‘𝐴) = (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)) |
13 | 12 | fveq1d 6498 |
. . . . 5
⊢ (𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘suc 𝐵)) |
14 | 13 | adantr 473 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘suc 𝐵)) |
15 | 12 | fveq1d 6498 |
. . . . . 6
⊢ (𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) |
16 | 15 | adantr 473 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) |
17 | 16 | unieqd 4718 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ∪ ((𝑈‘𝐴)‘𝐵) = ∪
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘𝐵)) |
18 | 10, 14, 17 | 3eqtr4d 2817 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
19 | | uni0 4735 |
. . . . 5
⊢ ∪ ∅ = ∅ |
20 | 19 | eqcomi 2780 |
. . . 4
⊢ ∅ =
∪ ∅ |
21 | 11 | itunifn 9635 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝑈‘𝐴) Fn ω) |
22 | | fndm 6285 |
. . . . . . . . . 10
⊢ ((𝑈‘𝐴) Fn ω → dom (𝑈‘𝐴) = ω) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → dom (𝑈‘𝐴) = ω) |
24 | 23 | eleq2d 2844 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (suc 𝐵 ∈ dom (𝑈‘𝐴) ↔ suc 𝐵 ∈ ω)) |
25 | | peano2b 7410 |
. . . . . . . 8
⊢ (𝐵 ∈ ω ↔ suc 𝐵 ∈
ω) |
26 | 24, 25 | syl6bbr 281 |
. . . . . . 7
⊢ (𝐴 ∈ V → (suc 𝐵 ∈ dom (𝑈‘𝐴) ↔ 𝐵 ∈ ω)) |
27 | 26 | notbid 310 |
. . . . . 6
⊢ (𝐴 ∈ V → (¬ suc
𝐵 ∈ dom (𝑈‘𝐴) ↔ ¬ 𝐵 ∈ ω)) |
28 | 27 | biimpar 470 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ¬
suc 𝐵 ∈ dom (𝑈‘𝐴)) |
29 | | ndmfv 6526 |
. . . . 5
⊢ (¬
suc 𝐵 ∈ dom (𝑈‘𝐴) → ((𝑈‘𝐴)‘suc 𝐵) = ∅) |
30 | 28, 29 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ∅) |
31 | 23 | eleq2d 2844 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (𝐵 ∈ dom (𝑈‘𝐴) ↔ 𝐵 ∈ ω)) |
32 | 31 | notbid 310 |
. . . . . . 7
⊢ (𝐴 ∈ V → (¬ 𝐵 ∈ dom (𝑈‘𝐴) ↔ ¬ 𝐵 ∈ ω)) |
33 | 32 | biimpar 470 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ¬
𝐵 ∈ dom (𝑈‘𝐴)) |
34 | | ndmfv 6526 |
. . . . . 6
⊢ (¬
𝐵 ∈ dom (𝑈‘𝐴) → ((𝑈‘𝐴)‘𝐵) = ∅) |
35 | 33, 34 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘𝐵) = ∅) |
36 | 35 | unieqd 4718 |
. . . 4
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ∪ ((𝑈‘𝐴)‘𝐵) = ∪
∅) |
37 | 20, 30, 36 | 3eqtr4a 2833 |
. . 3
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
38 | 18, 37 | pm2.61dan 801 |
. 2
⊢ (𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
39 | | 0fv 6536 |
. . . . 5
⊢
(∅‘𝐵) =
∅ |
40 | 39 | unieqi 4717 |
. . . 4
⊢ ∪ (∅‘𝐵) = ∪
∅ |
41 | | 0fv 6536 |
. . . 4
⊢
(∅‘suc 𝐵) = ∅ |
42 | 19, 40, 41 | 3eqtr4ri 2806 |
. . 3
⊢
(∅‘suc 𝐵) = ∪
(∅‘𝐵) |
43 | | fvprc 6489 |
. . . 4
⊢ (¬
𝐴 ∈ V → (𝑈‘𝐴) = ∅) |
44 | 43 | fveq1d 6498 |
. . 3
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = (∅‘suc 𝐵)) |
45 | 43 | fveq1d 6498 |
. . . 4
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) = (∅‘𝐵)) |
46 | 45 | unieqd 4718 |
. . 3
⊢ (¬
𝐴 ∈ V → ∪ ((𝑈‘𝐴)‘𝐵) = ∪
(∅‘𝐵)) |
47 | 42, 44, 46 | 3eqtr4a 2833 |
. 2
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
48 | 38, 47 | pm2.61i 177 |
1
⊢ ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵) |