Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . 4
⊢ (𝑏 = 𝐴 → (𝑈‘𝑏) = (𝑈‘𝐴)) |
2 | 1 | fveq1d 6105 |
. . 3
⊢ (𝑏 = 𝐴 → ((𝑈‘𝑏)‘suc 𝐵) = ((𝑈‘𝐴)‘suc 𝐵)) |
3 | | iuneq1 4470 |
. . 3
⊢ (𝑏 = 𝐴 → ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵) = ∪
𝑎 ∈ 𝐴 ((𝑈‘𝑎)‘𝐵)) |
4 | 2, 3 | eqeq12d 2625 |
. 2
⊢ (𝑏 = 𝐴 → (((𝑈‘𝑏)‘suc 𝐵) = ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵) ↔ ((𝑈‘𝐴)‘suc 𝐵) = ∪
𝑎 ∈ 𝐴 ((𝑈‘𝑎)‘𝐵))) |
5 | | suceq 5707 |
. . . . . 6
⊢ (𝑑 = ∅ → suc 𝑑 = suc ∅) |
6 | 5 | fveq2d 6107 |
. . . . 5
⊢ (𝑑 = ∅ → ((𝑈‘𝑏)‘suc 𝑑) = ((𝑈‘𝑏)‘suc ∅)) |
7 | | fveq2 6103 |
. . . . . 6
⊢ (𝑑 = ∅ → ((𝑈‘𝑎)‘𝑑) = ((𝑈‘𝑎)‘∅)) |
8 | 7 | iuneq2d 4483 |
. . . . 5
⊢ (𝑑 = ∅ → ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘∅)) |
9 | 6, 8 | eqeq12d 2625 |
. . . 4
⊢ (𝑑 = ∅ → (((𝑈‘𝑏)‘suc 𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) ↔ ((𝑈‘𝑏)‘suc ∅) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘∅))) |
10 | | suceq 5707 |
. . . . . 6
⊢ (𝑑 = 𝑐 → suc 𝑑 = suc 𝑐) |
11 | 10 | fveq2d 6107 |
. . . . 5
⊢ (𝑑 = 𝑐 → ((𝑈‘𝑏)‘suc 𝑑) = ((𝑈‘𝑏)‘suc 𝑐)) |
12 | | fveq2 6103 |
. . . . . 6
⊢ (𝑑 = 𝑐 → ((𝑈‘𝑎)‘𝑑) = ((𝑈‘𝑎)‘𝑐)) |
13 | 12 | iuneq2d 4483 |
. . . . 5
⊢ (𝑑 = 𝑐 → ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐)) |
14 | 11, 13 | eqeq12d 2625 |
. . . 4
⊢ (𝑑 = 𝑐 → (((𝑈‘𝑏)‘suc 𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) ↔ ((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐))) |
15 | | suceq 5707 |
. . . . . 6
⊢ (𝑑 = suc 𝑐 → suc 𝑑 = suc suc 𝑐) |
16 | 15 | fveq2d 6107 |
. . . . 5
⊢ (𝑑 = suc 𝑐 → ((𝑈‘𝑏)‘suc 𝑑) = ((𝑈‘𝑏)‘suc suc 𝑐)) |
17 | | fveq2 6103 |
. . . . . 6
⊢ (𝑑 = suc 𝑐 → ((𝑈‘𝑎)‘𝑑) = ((𝑈‘𝑎)‘suc 𝑐)) |
18 | 17 | iuneq2d 4483 |
. . . . 5
⊢ (𝑑 = suc 𝑐 → ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐)) |
19 | 16, 18 | eqeq12d 2625 |
. . . 4
⊢ (𝑑 = suc 𝑐 → (((𝑈‘𝑏)‘suc 𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) ↔ ((𝑈‘𝑏)‘suc suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐))) |
20 | | suceq 5707 |
. . . . . 6
⊢ (𝑑 = 𝐵 → suc 𝑑 = suc 𝐵) |
21 | 20 | fveq2d 6107 |
. . . . 5
⊢ (𝑑 = 𝐵 → ((𝑈‘𝑏)‘suc 𝑑) = ((𝑈‘𝑏)‘suc 𝐵)) |
22 | | fveq2 6103 |
. . . . . 6
⊢ (𝑑 = 𝐵 → ((𝑈‘𝑎)‘𝑑) = ((𝑈‘𝑎)‘𝐵)) |
23 | 22 | iuneq2d 4483 |
. . . . 5
⊢ (𝑑 = 𝐵 → ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵)) |
24 | 21, 23 | eqeq12d 2625 |
. . . 4
⊢ (𝑑 = 𝐵 → (((𝑈‘𝑏)‘suc 𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) ↔ ((𝑈‘𝑏)‘suc 𝐵) = ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵))) |
25 | | uniiun 4509 |
. . . . 5
⊢ ∪ 𝑏 =
∪ 𝑎 ∈ 𝑏 𝑎 |
26 | | ituni.u |
. . . . . . 7
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
27 | 26 | itunisuc 9124 |
. . . . . 6
⊢ ((𝑈‘𝑏)‘suc ∅) = ∪ ((𝑈‘𝑏)‘∅) |
28 | | vex 3176 |
. . . . . . . 8
⊢ 𝑏 ∈ V |
29 | 26 | ituni0 9123 |
. . . . . . . 8
⊢ (𝑏 ∈ V → ((𝑈‘𝑏)‘∅) = 𝑏) |
30 | 28, 29 | ax-mp 5 |
. . . . . . 7
⊢ ((𝑈‘𝑏)‘∅) = 𝑏 |
31 | 30 | unieqi 4381 |
. . . . . 6
⊢ ∪ ((𝑈‘𝑏)‘∅) = ∪ 𝑏 |
32 | 27, 31 | eqtri 2632 |
. . . . 5
⊢ ((𝑈‘𝑏)‘suc ∅) = ∪ 𝑏 |
33 | 26 | ituni0 9123 |
. . . . . 6
⊢ (𝑎 ∈ 𝑏 → ((𝑈‘𝑎)‘∅) = 𝑎) |
34 | 33 | iuneq2i 4475 |
. . . . 5
⊢ ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘∅) = ∪ 𝑎 ∈ 𝑏 𝑎 |
35 | 25, 32, 34 | 3eqtr4i 2642 |
. . . 4
⊢ ((𝑈‘𝑏)‘suc ∅) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘∅) |
36 | 26 | itunisuc 9124 |
. . . . . 6
⊢ ((𝑈‘𝑏)‘suc suc 𝑐) = ∪ ((𝑈‘𝑏)‘suc 𝑐) |
37 | | unieq 4380 |
. . . . . . 7
⊢ (((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) → ∪ ((𝑈‘𝑏)‘suc 𝑐) = ∪ ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐)) |
38 | 26 | itunisuc 9124 |
. . . . . . . . . 10
⊢ ((𝑈‘𝑎)‘suc 𝑐) = ∪ ((𝑈‘𝑎)‘𝑐) |
39 | 38 | a1i 11 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝑏 → ((𝑈‘𝑎)‘suc 𝑐) = ∪ ((𝑈‘𝑎)‘𝑐)) |
40 | 39 | iuneq2i 4475 |
. . . . . . . 8
⊢ ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ∪ ((𝑈‘𝑎)‘𝑐) |
41 | | iuncom4 4464 |
. . . . . . . 8
⊢ ∪ 𝑎 ∈ 𝑏 ∪ ((𝑈‘𝑎)‘𝑐) = ∪ ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) |
42 | 40, 41 | eqtr2i 2633 |
. . . . . . 7
⊢ ∪ ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐) |
43 | 37, 42 | syl6eq 2660 |
. . . . . 6
⊢ (((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) → ∪ ((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐)) |
44 | 36, 43 | syl5eq 2656 |
. . . . 5
⊢ (((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) → ((𝑈‘𝑏)‘suc suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐)) |
45 | 44 | a1i 11 |
. . . 4
⊢ (𝑐 ∈ ω → (((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) → ((𝑈‘𝑏)‘suc suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐))) |
46 | 9, 14, 19, 24, 35, 45 | finds 6984 |
. . 3
⊢ (𝐵 ∈ ω → ((𝑈‘𝑏)‘suc 𝐵) = ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵)) |
47 | | iun0 4512 |
. . . . 5
⊢ ∪ 𝑎 ∈ 𝑏 ∅ = ∅ |
48 | 47 | eqcomi 2619 |
. . . 4
⊢ ∅ =
∪ 𝑎 ∈ 𝑏 ∅ |
49 | | peano2b 6973 |
. . . . . 6
⊢ (𝐵 ∈ ω ↔ suc 𝐵 ∈
ω) |
50 | 26 | itunifn 9122 |
. . . . . . . 8
⊢ (𝑏 ∈ V → (𝑈‘𝑏) Fn ω) |
51 | | fndm 5904 |
. . . . . . . 8
⊢ ((𝑈‘𝑏) Fn ω → dom (𝑈‘𝑏) = ω) |
52 | 28, 50, 51 | mp2b 10 |
. . . . . . 7
⊢ dom
(𝑈‘𝑏) = ω |
53 | 52 | eleq2i 2680 |
. . . . . 6
⊢ (suc
𝐵 ∈ dom (𝑈‘𝑏) ↔ suc 𝐵 ∈ ω) |
54 | 49, 53 | bitr4i 266 |
. . . . 5
⊢ (𝐵 ∈ ω ↔ suc 𝐵 ∈ dom (𝑈‘𝑏)) |
55 | | ndmfv 6128 |
. . . . 5
⊢ (¬
suc 𝐵 ∈ dom (𝑈‘𝑏) → ((𝑈‘𝑏)‘suc 𝐵) = ∅) |
56 | 54, 55 | sylnbi 319 |
. . . 4
⊢ (¬
𝐵 ∈ ω →
((𝑈‘𝑏)‘suc 𝐵) = ∅) |
57 | | vex 3176 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
58 | 26 | itunifn 9122 |
. . . . . . . 8
⊢ (𝑎 ∈ V → (𝑈‘𝑎) Fn ω) |
59 | | fndm 5904 |
. . . . . . . 8
⊢ ((𝑈‘𝑎) Fn ω → dom (𝑈‘𝑎) = ω) |
60 | 57, 58, 59 | mp2b 10 |
. . . . . . 7
⊢ dom
(𝑈‘𝑎) = ω |
61 | 60 | eleq2i 2680 |
. . . . . 6
⊢ (𝐵 ∈ dom (𝑈‘𝑎) ↔ 𝐵 ∈ ω) |
62 | | ndmfv 6128 |
. . . . . 6
⊢ (¬
𝐵 ∈ dom (𝑈‘𝑎) → ((𝑈‘𝑎)‘𝐵) = ∅) |
63 | 61, 62 | sylnbir 320 |
. . . . 5
⊢ (¬
𝐵 ∈ ω →
((𝑈‘𝑎)‘𝐵) = ∅) |
64 | 63 | iuneq2d 4483 |
. . . 4
⊢ (¬
𝐵 ∈ ω →
∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵) = ∪
𝑎 ∈ 𝑏 ∅) |
65 | 48, 56, 64 | 3eqtr4a 2670 |
. . 3
⊢ (¬
𝐵 ∈ ω →
((𝑈‘𝑏)‘suc 𝐵) = ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵)) |
66 | 46, 65 | pm2.61i 175 |
. 2
⊢ ((𝑈‘𝑏)‘suc 𝐵) = ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵) |
67 | 4, 66 | vtoclg 3239 |
1
⊢ (𝐴 ∈ 𝑉 → ((𝑈‘𝐴)‘suc 𝐵) = ∪
𝑎 ∈ 𝐴 ((𝑈‘𝑎)‘𝐵)) |