| Step | Hyp | Ref
| Expression |
| 1 | | frsuc 8477 |
. . . . . 6
⊢ (𝐵 ∈ ω →
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘suc 𝐵) = ((𝑦 ∈ V ↦ ∪ 𝑦)‘((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵))) |
| 2 | | fvex 6919 |
. . . . . . 7
⊢
((rec((𝑦 ∈ V
↦ ∪ 𝑦), 𝐴) ↾ ω)‘𝐵) ∈ V |
| 3 | | unieq 4918 |
. . . . . . . 8
⊢ (𝑎 = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵) →
∪ 𝑎 = ∪ ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) |
| 4 | | unieq 4918 |
. . . . . . . . 9
⊢ (𝑦 = 𝑎 → ∪ 𝑦 = ∪
𝑎) |
| 5 | 4 | cbvmptv 5255 |
. . . . . . . 8
⊢ (𝑦 ∈ V ↦ ∪ 𝑦) =
(𝑎 ∈ V ↦ ∪ 𝑎) |
| 6 | 2 | uniex 7761 |
. . . . . . . 8
⊢ ∪ ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵) ∈
V |
| 7 | 3, 5, 6 | fvmpt 7016 |
. . . . . . 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 2793 |
. . . . 5
⊢ (𝐵 ∈ ω →
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘suc 𝐵) = ∪
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘𝐵)) |
| 10 | 9 | adantl 481 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) →
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘suc 𝐵) = ∪
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘𝐵)) |
| 11 | | ituni.u |
. . . . . . 7
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
| 12 | 11 | itunifval 10456 |
. . . . . 6
⊢ (𝐴 ∈ V → (𝑈‘𝐴) = (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)) |
| 13 | 12 | fveq1d 6908 |
. . . . 5
⊢ (𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘suc 𝐵)) |
| 14 | 13 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘suc 𝐵)) |
| 15 | 12 | fveq1d 6908 |
. . . . . 6
⊢ (𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) |
| 16 | 15 | adantr 480 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘𝐵) = ((rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝐴) ↾
ω)‘𝐵)) |
| 17 | 16 | unieqd 4920 |
. . . 4
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ∪ ((𝑈‘𝐴)‘𝐵) = ∪
((rec((𝑦 ∈ V ↦
∪ 𝑦), 𝐴) ↾ ω)‘𝐵)) |
| 18 | 10, 14, 17 | 3eqtr4d 2787 |
. . 3
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
| 19 | | uni0 4935 |
. . . . 5
⊢ ∪ ∅ = ∅ |
| 20 | 19 | eqcomi 2746 |
. . . 4
⊢ ∅ =
∪ ∅ |
| 21 | 11 | itunifn 10457 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝑈‘𝐴) Fn ω) |
| 22 | 21 | fndmd 6673 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → dom (𝑈‘𝐴) = ω) |
| 23 | 22 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (suc 𝐵 ∈ dom (𝑈‘𝐴) ↔ suc 𝐵 ∈ ω)) |
| 24 | | peano2b 7904 |
. . . . . . . 8
⊢ (𝐵 ∈ ω ↔ suc 𝐵 ∈
ω) |
| 25 | 23, 24 | bitr4di 289 |
. . . . . . 7
⊢ (𝐴 ∈ V → (suc 𝐵 ∈ dom (𝑈‘𝐴) ↔ 𝐵 ∈ ω)) |
| 26 | 25 | notbid 318 |
. . . . . 6
⊢ (𝐴 ∈ V → (¬ suc
𝐵 ∈ dom (𝑈‘𝐴) ↔ ¬ 𝐵 ∈ ω)) |
| 27 | 26 | biimpar 477 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ¬
suc 𝐵 ∈ dom (𝑈‘𝐴)) |
| 28 | | ndmfv 6941 |
. . . . 5
⊢ (¬
suc 𝐵 ∈ dom (𝑈‘𝐴) → ((𝑈‘𝐴)‘suc 𝐵) = ∅) |
| 29 | 27, 28 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ∅) |
| 30 | 22 | eleq2d 2827 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (𝐵 ∈ dom (𝑈‘𝐴) ↔ 𝐵 ∈ ω)) |
| 31 | 30 | notbid 318 |
. . . . . . 7
⊢ (𝐴 ∈ V → (¬ 𝐵 ∈ dom (𝑈‘𝐴) ↔ ¬ 𝐵 ∈ ω)) |
| 32 | 31 | biimpar 477 |
. . . . . 6
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ¬
𝐵 ∈ dom (𝑈‘𝐴)) |
| 33 | | ndmfv 6941 |
. . . . . 6
⊢ (¬
𝐵 ∈ dom (𝑈‘𝐴) → ((𝑈‘𝐴)‘𝐵) = ∅) |
| 34 | 32, 33 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘𝐵) = ∅) |
| 35 | 34 | unieqd 4920 |
. . . 4
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ∪ ((𝑈‘𝐴)‘𝐵) = ∪
∅) |
| 36 | 20, 29, 35 | 3eqtr4a 2803 |
. . 3
⊢ ((𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω) → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
| 37 | 18, 36 | pm2.61dan 813 |
. 2
⊢ (𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
| 38 | | 0fv 6950 |
. . . . 5
⊢
(∅‘𝐵) =
∅ |
| 39 | 38 | unieqi 4919 |
. . . 4
⊢ ∪ (∅‘𝐵) = ∪
∅ |
| 40 | | 0fv 6950 |
. . . 4
⊢
(∅‘suc 𝐵) = ∅ |
| 41 | 19, 39, 40 | 3eqtr4ri 2776 |
. . 3
⊢
(∅‘suc 𝐵) = ∪
(∅‘𝐵) |
| 42 | | fvprc 6898 |
. . . 4
⊢ (¬
𝐴 ∈ V → (𝑈‘𝐴) = ∅) |
| 43 | 42 | fveq1d 6908 |
. . 3
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = (∅‘suc 𝐵)) |
| 44 | 42 | fveq1d 6908 |
. . . 4
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) = (∅‘𝐵)) |
| 45 | 44 | unieqd 4920 |
. . 3
⊢ (¬
𝐴 ∈ V → ∪ ((𝑈‘𝐴)‘𝐵) = ∪
(∅‘𝐵)) |
| 46 | 41, 43, 45 | 3eqtr4a 2803 |
. 2
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵)) |
| 47 | 37, 46 | pm2.61i 182 |
1
⊢ ((𝑈‘𝐴)‘suc 𝐵) = ∪ ((𝑈‘𝐴)‘𝐵) |