Step | Hyp | Ref
| Expression |
1 | | fveq2 6675 |
. . . 4
⊢ (𝑏 = 𝐴 → (𝑈‘𝑏) = (𝑈‘𝐴)) |
2 | 1 | fveq1d 6677 |
. . 3
⊢ (𝑏 = 𝐴 → ((𝑈‘𝑏)‘suc 𝐵) = ((𝑈‘𝐴)‘suc 𝐵)) |
3 | | iuneq1 4898 |
. . 3
⊢ (𝑏 = 𝐴 → ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵) = ∪
𝑎 ∈ 𝐴 ((𝑈‘𝑎)‘𝐵)) |
4 | 2, 3 | eqeq12d 2754 |
. 2
⊢ (𝑏 = 𝐴 → (((𝑈‘𝑏)‘suc 𝐵) = ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵) ↔ ((𝑈‘𝐴)‘suc 𝐵) = ∪
𝑎 ∈ 𝐴 ((𝑈‘𝑎)‘𝐵))) |
5 | | suceq 6238 |
. . . . . 6
⊢ (𝑑 = ∅ → suc 𝑑 = suc ∅) |
6 | 5 | fveq2d 6679 |
. . . . 5
⊢ (𝑑 = ∅ → ((𝑈‘𝑏)‘suc 𝑑) = ((𝑈‘𝑏)‘suc ∅)) |
7 | | fveq2 6675 |
. . . . . 6
⊢ (𝑑 = ∅ → ((𝑈‘𝑎)‘𝑑) = ((𝑈‘𝑎)‘∅)) |
8 | 7 | iuneq2d 4911 |
. . . . 5
⊢ (𝑑 = ∅ → ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘∅)) |
9 | 6, 8 | eqeq12d 2754 |
. . . 4
⊢ (𝑑 = ∅ → (((𝑈‘𝑏)‘suc 𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) ↔ ((𝑈‘𝑏)‘suc ∅) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘∅))) |
10 | | suceq 6238 |
. . . . . 6
⊢ (𝑑 = 𝑐 → suc 𝑑 = suc 𝑐) |
11 | 10 | fveq2d 6679 |
. . . . 5
⊢ (𝑑 = 𝑐 → ((𝑈‘𝑏)‘suc 𝑑) = ((𝑈‘𝑏)‘suc 𝑐)) |
12 | | fveq2 6675 |
. . . . . 6
⊢ (𝑑 = 𝑐 → ((𝑈‘𝑎)‘𝑑) = ((𝑈‘𝑎)‘𝑐)) |
13 | 12 | iuneq2d 4911 |
. . . . 5
⊢ (𝑑 = 𝑐 → ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐)) |
14 | 11, 13 | eqeq12d 2754 |
. . . 4
⊢ (𝑑 = 𝑐 → (((𝑈‘𝑏)‘suc 𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) ↔ ((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐))) |
15 | | suceq 6238 |
. . . . . 6
⊢ (𝑑 = suc 𝑐 → suc 𝑑 = suc suc 𝑐) |
16 | 15 | fveq2d 6679 |
. . . . 5
⊢ (𝑑 = suc 𝑐 → ((𝑈‘𝑏)‘suc 𝑑) = ((𝑈‘𝑏)‘suc suc 𝑐)) |
17 | | fveq2 6675 |
. . . . . 6
⊢ (𝑑 = suc 𝑐 → ((𝑈‘𝑎)‘𝑑) = ((𝑈‘𝑎)‘suc 𝑐)) |
18 | 17 | iuneq2d 4911 |
. . . . 5
⊢ (𝑑 = suc 𝑐 → ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐)) |
19 | 16, 18 | eqeq12d 2754 |
. . . 4
⊢ (𝑑 = suc 𝑐 → (((𝑈‘𝑏)‘suc 𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) ↔ ((𝑈‘𝑏)‘suc suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐))) |
20 | | suceq 6238 |
. . . . . 6
⊢ (𝑑 = 𝐵 → suc 𝑑 = suc 𝐵) |
21 | 20 | fveq2d 6679 |
. . . . 5
⊢ (𝑑 = 𝐵 → ((𝑈‘𝑏)‘suc 𝑑) = ((𝑈‘𝑏)‘suc 𝐵)) |
22 | | fveq2 6675 |
. . . . . 6
⊢ (𝑑 = 𝐵 → ((𝑈‘𝑎)‘𝑑) = ((𝑈‘𝑎)‘𝐵)) |
23 | 22 | iuneq2d 4911 |
. . . . 5
⊢ (𝑑 = 𝐵 → ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵)) |
24 | 21, 23 | eqeq12d 2754 |
. . . 4
⊢ (𝑑 = 𝐵 → (((𝑈‘𝑏)‘suc 𝑑) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑑) ↔ ((𝑈‘𝑏)‘suc 𝐵) = ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵))) |
25 | | uniiun 4945 |
. . . . 5
⊢ ∪ 𝑏 =
∪ 𝑎 ∈ 𝑏 𝑎 |
26 | | ituni.u |
. . . . . . 7
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
27 | 26 | itunisuc 9920 |
. . . . . 6
⊢ ((𝑈‘𝑏)‘suc ∅) = ∪ ((𝑈‘𝑏)‘∅) |
28 | 26 | ituni0 9919 |
. . . . . . . 8
⊢ (𝑏 ∈ V → ((𝑈‘𝑏)‘∅) = 𝑏) |
29 | 28 | elv 3404 |
. . . . . . 7
⊢ ((𝑈‘𝑏)‘∅) = 𝑏 |
30 | 29 | unieqi 4810 |
. . . . . 6
⊢ ∪ ((𝑈‘𝑏)‘∅) = ∪ 𝑏 |
31 | 27, 30 | eqtri 2761 |
. . . . 5
⊢ ((𝑈‘𝑏)‘suc ∅) = ∪ 𝑏 |
32 | 26 | ituni0 9919 |
. . . . . 6
⊢ (𝑎 ∈ 𝑏 → ((𝑈‘𝑎)‘∅) = 𝑎) |
33 | 32 | iuneq2i 4903 |
. . . . 5
⊢ ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘∅) = ∪ 𝑎 ∈ 𝑏 𝑎 |
34 | 25, 31, 33 | 3eqtr4i 2771 |
. . . 4
⊢ ((𝑈‘𝑏)‘suc ∅) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘∅) |
35 | 26 | itunisuc 9920 |
. . . . . 6
⊢ ((𝑈‘𝑏)‘suc suc 𝑐) = ∪ ((𝑈‘𝑏)‘suc 𝑐) |
36 | | unieq 4808 |
. . . . . . 7
⊢ (((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) → ∪ ((𝑈‘𝑏)‘suc 𝑐) = ∪ ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐)) |
37 | 26 | itunisuc 9920 |
. . . . . . . . . 10
⊢ ((𝑈‘𝑎)‘suc 𝑐) = ∪ ((𝑈‘𝑎)‘𝑐) |
38 | 37 | a1i 11 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝑏 → ((𝑈‘𝑎)‘suc 𝑐) = ∪ ((𝑈‘𝑎)‘𝑐)) |
39 | 38 | iuneq2i 4903 |
. . . . . . . 8
⊢ ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ∪ ((𝑈‘𝑎)‘𝑐) |
40 | | iuncom4 4890 |
. . . . . . . 8
⊢ ∪ 𝑎 ∈ 𝑏 ∪ ((𝑈‘𝑎)‘𝑐) = ∪ ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) |
41 | 39, 40 | eqtr2i 2762 |
. . . . . . 7
⊢ ∪ ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐) |
42 | 36, 41 | eqtrdi 2789 |
. . . . . 6
⊢ (((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) → ∪ ((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐)) |
43 | 35, 42 | syl5eq 2785 |
. . . . 5
⊢ (((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) → ((𝑈‘𝑏)‘suc suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐)) |
44 | 43 | a1i 11 |
. . . 4
⊢ (𝑐 ∈ ω → (((𝑈‘𝑏)‘suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝑐) → ((𝑈‘𝑏)‘suc suc 𝑐) = ∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘suc 𝑐))) |
45 | 9, 14, 19, 24, 34, 44 | finds 7630 |
. . 3
⊢ (𝐵 ∈ ω → ((𝑈‘𝑏)‘suc 𝐵) = ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵)) |
46 | | iun0 4948 |
. . . . 5
⊢ ∪ 𝑎 ∈ 𝑏 ∅ = ∅ |
47 | 46 | eqcomi 2747 |
. . . 4
⊢ ∅ =
∪ 𝑎 ∈ 𝑏 ∅ |
48 | | peano2b 7616 |
. . . . . 6
⊢ (𝐵 ∈ ω ↔ suc 𝐵 ∈
ω) |
49 | | vex 3402 |
. . . . . . . 8
⊢ 𝑏 ∈ V |
50 | 26 | itunifn 9918 |
. . . . . . . 8
⊢ (𝑏 ∈ V → (𝑈‘𝑏) Fn ω) |
51 | | fndm 6441 |
. . . . . . . 8
⊢ ((𝑈‘𝑏) Fn ω → dom (𝑈‘𝑏) = ω) |
52 | 49, 50, 51 | mp2b 10 |
. . . . . . 7
⊢ dom
(𝑈‘𝑏) = ω |
53 | 52 | eleq2i 2824 |
. . . . . 6
⊢ (suc
𝐵 ∈ dom (𝑈‘𝑏) ↔ suc 𝐵 ∈ ω) |
54 | 48, 53 | bitr4i 281 |
. . . . 5
⊢ (𝐵 ∈ ω ↔ suc 𝐵 ∈ dom (𝑈‘𝑏)) |
55 | | ndmfv 6705 |
. . . . 5
⊢ (¬
suc 𝐵 ∈ dom (𝑈‘𝑏) → ((𝑈‘𝑏)‘suc 𝐵) = ∅) |
56 | 54, 55 | sylnbi 333 |
. . . 4
⊢ (¬
𝐵 ∈ ω →
((𝑈‘𝑏)‘suc 𝐵) = ∅) |
57 | | vex 3402 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
58 | 26 | itunifn 9918 |
. . . . . . . 8
⊢ (𝑎 ∈ V → (𝑈‘𝑎) Fn ω) |
59 | | fndm 6441 |
. . . . . . . 8
⊢ ((𝑈‘𝑎) Fn ω → dom (𝑈‘𝑎) = ω) |
60 | 57, 58, 59 | mp2b 10 |
. . . . . . 7
⊢ dom
(𝑈‘𝑎) = ω |
61 | 60 | eleq2i 2824 |
. . . . . 6
⊢ (𝐵 ∈ dom (𝑈‘𝑎) ↔ 𝐵 ∈ ω) |
62 | | ndmfv 6705 |
. . . . . 6
⊢ (¬
𝐵 ∈ dom (𝑈‘𝑎) → ((𝑈‘𝑎)‘𝐵) = ∅) |
63 | 61, 62 | sylnbir 334 |
. . . . 5
⊢ (¬
𝐵 ∈ ω →
((𝑈‘𝑎)‘𝐵) = ∅) |
64 | 63 | iuneq2d 4911 |
. . . 4
⊢ (¬
𝐵 ∈ ω →
∪ 𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵) = ∪
𝑎 ∈ 𝑏 ∅) |
65 | 47, 56, 64 | 3eqtr4a 2799 |
. . 3
⊢ (¬
𝐵 ∈ ω →
((𝑈‘𝑏)‘suc 𝐵) = ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵)) |
66 | 45, 65 | pm2.61i 185 |
. 2
⊢ ((𝑈‘𝑏)‘suc 𝐵) = ∪
𝑎 ∈ 𝑏 ((𝑈‘𝑎)‘𝐵) |
67 | 4, 66 | vtoclg 3471 |
1
⊢ (𝐴 ∈ 𝑉 → ((𝑈‘𝐴)‘suc 𝐵) = ∪
𝑎 ∈ 𝐴 ((𝑈‘𝑎)‘𝐵)) |