| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . 4
⊢ (𝑎 = 𝐴 → (TC‘𝑎) = (TC‘𝐴)) |
| 2 | | fveq2 6906 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑈‘𝑎) = (𝑈‘𝐴)) |
| 3 | 2 | rneqd 5949 |
. . . . 5
⊢ (𝑎 = 𝐴 → ran (𝑈‘𝑎) = ran (𝑈‘𝐴)) |
| 4 | 3 | unieqd 4920 |
. . . 4
⊢ (𝑎 = 𝐴 → ∪ ran
(𝑈‘𝑎) = ∪ ran (𝑈‘𝐴)) |
| 5 | 1, 4 | eqeq12d 2753 |
. . 3
⊢ (𝑎 = 𝐴 → ((TC‘𝑎) = ∪ ran (𝑈‘𝑎) ↔ (TC‘𝐴) = ∪ ran (𝑈‘𝐴))) |
| 6 | | ituni.u |
. . . . . . . 8
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
| 7 | 6 | ituni0 10458 |
. . . . . . 7
⊢ (𝑎 ∈ V → ((𝑈‘𝑎)‘∅) = 𝑎) |
| 8 | 7 | elv 3485 |
. . . . . 6
⊢ ((𝑈‘𝑎)‘∅) = 𝑎 |
| 9 | | fvssunirn 6939 |
. . . . . 6
⊢ ((𝑈‘𝑎)‘∅) ⊆ ∪ ran (𝑈‘𝑎) |
| 10 | 8, 9 | eqsstrri 4031 |
. . . . 5
⊢ 𝑎 ⊆ ∪ ran (𝑈‘𝑎) |
| 11 | | dftr3 5265 |
. . . . . 6
⊢ (Tr ∪ ran (𝑈‘𝑎) ↔ ∀𝑏 ∈ ∪ ran
(𝑈‘𝑎)𝑏 ⊆ ∪ ran
(𝑈‘𝑎)) |
| 12 | | vex 3484 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
| 13 | 6 | itunifn 10457 |
. . . . . . . 8
⊢ (𝑎 ∈ V → (𝑈‘𝑎) Fn ω) |
| 14 | | fnunirn 7274 |
. . . . . . . 8
⊢ ((𝑈‘𝑎) Fn ω → (𝑏 ∈ ∪ ran
(𝑈‘𝑎) ↔ ∃𝑐 ∈ ω 𝑏 ∈ ((𝑈‘𝑎)‘𝑐))) |
| 15 | 12, 13, 14 | mp2b 10 |
. . . . . . 7
⊢ (𝑏 ∈ ∪ ran (𝑈‘𝑎) ↔ ∃𝑐 ∈ ω 𝑏 ∈ ((𝑈‘𝑎)‘𝑐)) |
| 16 | | elssuni 4937 |
. . . . . . . . 9
⊢ (𝑏 ∈ ((𝑈‘𝑎)‘𝑐) → 𝑏 ⊆ ∪ ((𝑈‘𝑎)‘𝑐)) |
| 17 | 6 | itunisuc 10459 |
. . . . . . . . . 10
⊢ ((𝑈‘𝑎)‘suc 𝑐) = ∪ ((𝑈‘𝑎)‘𝑐) |
| 18 | | fvssunirn 6939 |
. . . . . . . . . 10
⊢ ((𝑈‘𝑎)‘suc 𝑐) ⊆ ∪ ran
(𝑈‘𝑎) |
| 19 | 17, 18 | eqsstrri 4031 |
. . . . . . . . 9
⊢ ∪ ((𝑈‘𝑎)‘𝑐) ⊆ ∪ ran
(𝑈‘𝑎) |
| 20 | 16, 19 | sstrdi 3996 |
. . . . . . . 8
⊢ (𝑏 ∈ ((𝑈‘𝑎)‘𝑐) → 𝑏 ⊆ ∪ ran
(𝑈‘𝑎)) |
| 21 | 20 | rexlimivw 3151 |
. . . . . . 7
⊢
(∃𝑐 ∈
ω 𝑏 ∈ ((𝑈‘𝑎)‘𝑐) → 𝑏 ⊆ ∪ ran
(𝑈‘𝑎)) |
| 22 | 15, 21 | sylbi 217 |
. . . . . 6
⊢ (𝑏 ∈ ∪ ran (𝑈‘𝑎) → 𝑏 ⊆ ∪ ran
(𝑈‘𝑎)) |
| 23 | 11, 22 | mprgbir 3068 |
. . . . 5
⊢ Tr ∪ ran (𝑈‘𝑎) |
| 24 | | tcmin 9781 |
. . . . . 6
⊢ (𝑎 ∈ V → ((𝑎 ⊆ ∪ ran (𝑈‘𝑎) ∧ Tr ∪ ran
(𝑈‘𝑎)) → (TC‘𝑎) ⊆ ∪ ran
(𝑈‘𝑎))) |
| 25 | 24 | elv 3485 |
. . . . 5
⊢ ((𝑎 ⊆ ∪ ran (𝑈‘𝑎) ∧ Tr ∪ ran
(𝑈‘𝑎)) → (TC‘𝑎) ⊆ ∪ ran
(𝑈‘𝑎)) |
| 26 | 10, 23, 25 | mp2an 692 |
. . . 4
⊢
(TC‘𝑎) ⊆
∪ ran (𝑈‘𝑎) |
| 27 | | unissb 4939 |
. . . . 5
⊢ (∪ ran (𝑈‘𝑎) ⊆ (TC‘𝑎) ↔ ∀𝑏 ∈ ran (𝑈‘𝑎)𝑏 ⊆ (TC‘𝑎)) |
| 28 | | fvelrnb 6969 |
. . . . . . 7
⊢ ((𝑈‘𝑎) Fn ω → (𝑏 ∈ ran (𝑈‘𝑎) ↔ ∃𝑐 ∈ ω ((𝑈‘𝑎)‘𝑐) = 𝑏)) |
| 29 | 12, 13, 28 | mp2b 10 |
. . . . . 6
⊢ (𝑏 ∈ ran (𝑈‘𝑎) ↔ ∃𝑐 ∈ ω ((𝑈‘𝑎)‘𝑐) = 𝑏) |
| 30 | 6 | itunitc1 10460 |
. . . . . . . . 9
⊢ ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎) |
| 31 | 30 | a1i 11 |
. . . . . . . 8
⊢ (𝑐 ∈ ω → ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎)) |
| 32 | | sseq1 4009 |
. . . . . . . 8
⊢ (((𝑈‘𝑎)‘𝑐) = 𝑏 → (((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎) ↔ 𝑏 ⊆ (TC‘𝑎))) |
| 33 | 31, 32 | syl5ibcom 245 |
. . . . . . 7
⊢ (𝑐 ∈ ω → (((𝑈‘𝑎)‘𝑐) = 𝑏 → 𝑏 ⊆ (TC‘𝑎))) |
| 34 | 33 | rexlimiv 3148 |
. . . . . 6
⊢
(∃𝑐 ∈
ω ((𝑈‘𝑎)‘𝑐) = 𝑏 → 𝑏 ⊆ (TC‘𝑎)) |
| 35 | 29, 34 | sylbi 217 |
. . . . 5
⊢ (𝑏 ∈ ran (𝑈‘𝑎) → 𝑏 ⊆ (TC‘𝑎)) |
| 36 | 27, 35 | mprgbir 3068 |
. . . 4
⊢ ∪ ran (𝑈‘𝑎) ⊆ (TC‘𝑎) |
| 37 | 26, 36 | eqssi 4000 |
. . 3
⊢
(TC‘𝑎) = ∪ ran (𝑈‘𝑎) |
| 38 | 5, 37 | vtoclg 3554 |
. 2
⊢ (𝐴 ∈ V → (TC‘𝐴) = ∪
ran (𝑈‘𝐴)) |
| 39 | | rn0 5936 |
. . . . 5
⊢ ran
∅ = ∅ |
| 40 | 39 | unieqi 4919 |
. . . 4
⊢ ∪ ran ∅ = ∪
∅ |
| 41 | | uni0 4935 |
. . . 4
⊢ ∪ ∅ = ∅ |
| 42 | 40, 41 | eqtr2i 2766 |
. . 3
⊢ ∅ =
∪ ran ∅ |
| 43 | | fvprc 6898 |
. . 3
⊢ (¬
𝐴 ∈ V →
(TC‘𝐴) =
∅) |
| 44 | | fvprc 6898 |
. . . . 5
⊢ (¬
𝐴 ∈ V → (𝑈‘𝐴) = ∅) |
| 45 | 44 | rneqd 5949 |
. . . 4
⊢ (¬
𝐴 ∈ V → ran
(𝑈‘𝐴) = ran ∅) |
| 46 | 45 | unieqd 4920 |
. . 3
⊢ (¬
𝐴 ∈ V → ∪ ran (𝑈‘𝐴) = ∪ ran
∅) |
| 47 | 42, 43, 46 | 3eqtr4a 2803 |
. 2
⊢ (¬
𝐴 ∈ V →
(TC‘𝐴) = ∪ ran (𝑈‘𝐴)) |
| 48 | 38, 47 | pm2.61i 182 |
1
⊢
(TC‘𝐴) = ∪ ran (𝑈‘𝐴) |