Step | Hyp | Ref
| Expression |
1 | | fveq2 6717 |
. . . 4
⊢ (𝑎 = 𝐴 → (TC‘𝑎) = (TC‘𝐴)) |
2 | | fveq2 6717 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑈‘𝑎) = (𝑈‘𝐴)) |
3 | 2 | rneqd 5807 |
. . . . 5
⊢ (𝑎 = 𝐴 → ran (𝑈‘𝑎) = ran (𝑈‘𝐴)) |
4 | 3 | unieqd 4833 |
. . . 4
⊢ (𝑎 = 𝐴 → ∪ ran
(𝑈‘𝑎) = ∪ ran (𝑈‘𝐴)) |
5 | 1, 4 | eqeq12d 2753 |
. . 3
⊢ (𝑎 = 𝐴 → ((TC‘𝑎) = ∪ ran (𝑈‘𝑎) ↔ (TC‘𝐴) = ∪ ran (𝑈‘𝐴))) |
6 | | ituni.u |
. . . . . . . 8
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
7 | 6 | ituni0 10032 |
. . . . . . 7
⊢ (𝑎 ∈ V → ((𝑈‘𝑎)‘∅) = 𝑎) |
8 | 7 | elv 3414 |
. . . . . 6
⊢ ((𝑈‘𝑎)‘∅) = 𝑎 |
9 | | fvssunirn 6746 |
. . . . . 6
⊢ ((𝑈‘𝑎)‘∅) ⊆ ∪ ran (𝑈‘𝑎) |
10 | 8, 9 | eqsstrri 3936 |
. . . . 5
⊢ 𝑎 ⊆ ∪ ran (𝑈‘𝑎) |
11 | | dftr3 5165 |
. . . . . 6
⊢ (Tr ∪ ran (𝑈‘𝑎) ↔ ∀𝑏 ∈ ∪ ran
(𝑈‘𝑎)𝑏 ⊆ ∪ ran
(𝑈‘𝑎)) |
12 | | vex 3412 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
13 | 6 | itunifn 10031 |
. . . . . . . 8
⊢ (𝑎 ∈ V → (𝑈‘𝑎) Fn ω) |
14 | | fnunirn 7066 |
. . . . . . . 8
⊢ ((𝑈‘𝑎) Fn ω → (𝑏 ∈ ∪ ran
(𝑈‘𝑎) ↔ ∃𝑐 ∈ ω 𝑏 ∈ ((𝑈‘𝑎)‘𝑐))) |
15 | 12, 13, 14 | mp2b 10 |
. . . . . . 7
⊢ (𝑏 ∈ ∪ ran (𝑈‘𝑎) ↔ ∃𝑐 ∈ ω 𝑏 ∈ ((𝑈‘𝑎)‘𝑐)) |
16 | | elssuni 4851 |
. . . . . . . . 9
⊢ (𝑏 ∈ ((𝑈‘𝑎)‘𝑐) → 𝑏 ⊆ ∪ ((𝑈‘𝑎)‘𝑐)) |
17 | 6 | itunisuc 10033 |
. . . . . . . . . 10
⊢ ((𝑈‘𝑎)‘suc 𝑐) = ∪ ((𝑈‘𝑎)‘𝑐) |
18 | | fvssunirn 6746 |
. . . . . . . . . 10
⊢ ((𝑈‘𝑎)‘suc 𝑐) ⊆ ∪ ran
(𝑈‘𝑎) |
19 | 17, 18 | eqsstrri 3936 |
. . . . . . . . 9
⊢ ∪ ((𝑈‘𝑎)‘𝑐) ⊆ ∪ ran
(𝑈‘𝑎) |
20 | 16, 19 | sstrdi 3913 |
. . . . . . . 8
⊢ (𝑏 ∈ ((𝑈‘𝑎)‘𝑐) → 𝑏 ⊆ ∪ ran
(𝑈‘𝑎)) |
21 | 20 | rexlimivw 3201 |
. . . . . . 7
⊢
(∃𝑐 ∈
ω 𝑏 ∈ ((𝑈‘𝑎)‘𝑐) → 𝑏 ⊆ ∪ ran
(𝑈‘𝑎)) |
22 | 15, 21 | sylbi 220 |
. . . . . 6
⊢ (𝑏 ∈ ∪ ran (𝑈‘𝑎) → 𝑏 ⊆ ∪ ran
(𝑈‘𝑎)) |
23 | 11, 22 | mprgbir 3076 |
. . . . 5
⊢ Tr ∪ ran (𝑈‘𝑎) |
24 | | tcmin 9357 |
. . . . . 6
⊢ (𝑎 ∈ V → ((𝑎 ⊆ ∪ ran (𝑈‘𝑎) ∧ Tr ∪ ran
(𝑈‘𝑎)) → (TC‘𝑎) ⊆ ∪ ran
(𝑈‘𝑎))) |
25 | 24 | elv 3414 |
. . . . 5
⊢ ((𝑎 ⊆ ∪ ran (𝑈‘𝑎) ∧ Tr ∪ ran
(𝑈‘𝑎)) → (TC‘𝑎) ⊆ ∪ ran
(𝑈‘𝑎)) |
26 | 10, 23, 25 | mp2an 692 |
. . . 4
⊢
(TC‘𝑎) ⊆
∪ ran (𝑈‘𝑎) |
27 | | unissb 4853 |
. . . . 5
⊢ (∪ ran (𝑈‘𝑎) ⊆ (TC‘𝑎) ↔ ∀𝑏 ∈ ran (𝑈‘𝑎)𝑏 ⊆ (TC‘𝑎)) |
28 | | fvelrnb 6773 |
. . . . . . 7
⊢ ((𝑈‘𝑎) Fn ω → (𝑏 ∈ ran (𝑈‘𝑎) ↔ ∃𝑐 ∈ ω ((𝑈‘𝑎)‘𝑐) = 𝑏)) |
29 | 12, 13, 28 | mp2b 10 |
. . . . . 6
⊢ (𝑏 ∈ ran (𝑈‘𝑎) ↔ ∃𝑐 ∈ ω ((𝑈‘𝑎)‘𝑐) = 𝑏) |
30 | 6 | itunitc1 10034 |
. . . . . . . . 9
⊢ ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎) |
31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (𝑐 ∈ ω → ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎)) |
32 | | sseq1 3926 |
. . . . . . . 8
⊢ (((𝑈‘𝑎)‘𝑐) = 𝑏 → (((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎) ↔ 𝑏 ⊆ (TC‘𝑎))) |
33 | 31, 32 | syl5ibcom 248 |
. . . . . . 7
⊢ (𝑐 ∈ ω → (((𝑈‘𝑎)‘𝑐) = 𝑏 → 𝑏 ⊆ (TC‘𝑎))) |
34 | 33 | rexlimiv 3199 |
. . . . . 6
⊢
(∃𝑐 ∈
ω ((𝑈‘𝑎)‘𝑐) = 𝑏 → 𝑏 ⊆ (TC‘𝑎)) |
35 | 29, 34 | sylbi 220 |
. . . . 5
⊢ (𝑏 ∈ ran (𝑈‘𝑎) → 𝑏 ⊆ (TC‘𝑎)) |
36 | 27, 35 | mprgbir 3076 |
. . . 4
⊢ ∪ ran (𝑈‘𝑎) ⊆ (TC‘𝑎) |
37 | 26, 36 | eqssi 3917 |
. . 3
⊢
(TC‘𝑎) = ∪ ran (𝑈‘𝑎) |
38 | 5, 37 | vtoclg 3481 |
. 2
⊢ (𝐴 ∈ V → (TC‘𝐴) = ∪
ran (𝑈‘𝐴)) |
39 | | rn0 5795 |
. . . . 5
⊢ ran
∅ = ∅ |
40 | 39 | unieqi 4832 |
. . . 4
⊢ ∪ ran ∅ = ∪
∅ |
41 | | uni0 4849 |
. . . 4
⊢ ∪ ∅ = ∅ |
42 | 40, 41 | eqtr2i 2766 |
. . 3
⊢ ∅ =
∪ ran ∅ |
43 | | fvprc 6709 |
. . 3
⊢ (¬
𝐴 ∈ V →
(TC‘𝐴) =
∅) |
44 | | fvprc 6709 |
. . . . 5
⊢ (¬
𝐴 ∈ V → (𝑈‘𝐴) = ∅) |
45 | 44 | rneqd 5807 |
. . . 4
⊢ (¬
𝐴 ∈ V → ran
(𝑈‘𝐴) = ran ∅) |
46 | 45 | unieqd 4833 |
. . 3
⊢ (¬
𝐴 ∈ V → ∪ ran (𝑈‘𝐴) = ∪ ran
∅) |
47 | 42, 43, 46 | 3eqtr4a 2804 |
. 2
⊢ (¬
𝐴 ∈ V →
(TC‘𝐴) = ∪ ran (𝑈‘𝐴)) |
48 | 38, 47 | pm2.61i 185 |
1
⊢
(TC‘𝐴) = ∪ ran (𝑈‘𝐴) |