Step | Hyp | Ref
| Expression |
1 | | fveq2 6191 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑈‘𝑎) = (𝑈‘𝐴)) |
2 | 1 | fveq1d 6193 |
. . . 4
⊢ (𝑎 = 𝐴 → ((𝑈‘𝑎)‘𝐵) = ((𝑈‘𝐴)‘𝐵)) |
3 | | fveq2 6191 |
. . . 4
⊢ (𝑎 = 𝐴 → (TC‘𝑎) = (TC‘𝐴)) |
4 | 2, 3 | sseq12d 3634 |
. . 3
⊢ (𝑎 = 𝐴 → (((𝑈‘𝑎)‘𝐵) ⊆ (TC‘𝑎) ↔ ((𝑈‘𝐴)‘𝐵) ⊆ (TC‘𝐴))) |
5 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = ∅ → ((𝑈‘𝑎)‘𝑏) = ((𝑈‘𝑎)‘∅)) |
6 | 5 | sseq1d 3632 |
. . . . 5
⊢ (𝑏 = ∅ → (((𝑈‘𝑎)‘𝑏) ⊆ (TC‘𝑎) ↔ ((𝑈‘𝑎)‘∅) ⊆ (TC‘𝑎))) |
7 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = 𝑐 → ((𝑈‘𝑎)‘𝑏) = ((𝑈‘𝑎)‘𝑐)) |
8 | 7 | sseq1d 3632 |
. . . . 5
⊢ (𝑏 = 𝑐 → (((𝑈‘𝑎)‘𝑏) ⊆ (TC‘𝑎) ↔ ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎))) |
9 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = suc 𝑐 → ((𝑈‘𝑎)‘𝑏) = ((𝑈‘𝑎)‘suc 𝑐)) |
10 | 9 | sseq1d 3632 |
. . . . 5
⊢ (𝑏 = suc 𝑐 → (((𝑈‘𝑎)‘𝑏) ⊆ (TC‘𝑎) ↔ ((𝑈‘𝑎)‘suc 𝑐) ⊆ (TC‘𝑎))) |
11 | | fveq2 6191 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝑈‘𝑎)‘𝑏) = ((𝑈‘𝑎)‘𝐵)) |
12 | 11 | sseq1d 3632 |
. . . . 5
⊢ (𝑏 = 𝐵 → (((𝑈‘𝑎)‘𝑏) ⊆ (TC‘𝑎) ↔ ((𝑈‘𝑎)‘𝐵) ⊆ (TC‘𝑎))) |
13 | | vex 3203 |
. . . . . 6
⊢ 𝑎 ∈ V |
14 | | ituni.u |
. . . . . . . 8
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
15 | 14 | ituni0 9240 |
. . . . . . 7
⊢ (𝑎 ∈ V → ((𝑈‘𝑎)‘∅) = 𝑎) |
16 | | tcid 8615 |
. . . . . . 7
⊢ (𝑎 ∈ V → 𝑎 ⊆ (TC‘𝑎)) |
17 | 15, 16 | eqsstrd 3639 |
. . . . . 6
⊢ (𝑎 ∈ V → ((𝑈‘𝑎)‘∅) ⊆ (TC‘𝑎)) |
18 | 13, 17 | ax-mp 5 |
. . . . 5
⊢ ((𝑈‘𝑎)‘∅) ⊆ (TC‘𝑎) |
19 | 14 | itunisuc 9241 |
. . . . . . 7
⊢ ((𝑈‘𝑎)‘suc 𝑐) = ∪ ((𝑈‘𝑎)‘𝑐) |
20 | | tctr 8616 |
. . . . . . . . . 10
⊢ Tr
(TC‘𝑎) |
21 | | pwtr 4921 |
. . . . . . . . . 10
⊢ (Tr
(TC‘𝑎) ↔ Tr
𝒫 (TC‘𝑎)) |
22 | 20, 21 | mpbi 220 |
. . . . . . . . 9
⊢ Tr
𝒫 (TC‘𝑎) |
23 | | trss 4761 |
. . . . . . . . 9
⊢ (Tr
𝒫 (TC‘𝑎)
→ (((𝑈‘𝑎)‘𝑐) ∈ 𝒫 (TC‘𝑎) → ((𝑈‘𝑎)‘𝑐) ⊆ 𝒫 (TC‘𝑎))) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . 8
⊢ (((𝑈‘𝑎)‘𝑐) ∈ 𝒫 (TC‘𝑎) → ((𝑈‘𝑎)‘𝑐) ⊆ 𝒫 (TC‘𝑎)) |
25 | | fvex 6201 |
. . . . . . . . 9
⊢ ((𝑈‘𝑎)‘𝑐) ∈ V |
26 | 25 | elpw 4164 |
. . . . . . . 8
⊢ (((𝑈‘𝑎)‘𝑐) ∈ 𝒫 (TC‘𝑎) ↔ ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎)) |
27 | | sspwuni 4611 |
. . . . . . . 8
⊢ (((𝑈‘𝑎)‘𝑐) ⊆ 𝒫 (TC‘𝑎) ↔ ∪ ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎)) |
28 | 24, 26, 27 | 3imtr3i 280 |
. . . . . . 7
⊢ (((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎) → ∪ ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎)) |
29 | 19, 28 | syl5eqss 3649 |
. . . . . 6
⊢ (((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎) → ((𝑈‘𝑎)‘suc 𝑐) ⊆ (TC‘𝑎)) |
30 | 29 | a1i 11 |
. . . . 5
⊢ (𝑐 ∈ ω → (((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎) → ((𝑈‘𝑎)‘suc 𝑐) ⊆ (TC‘𝑎))) |
31 | 6, 8, 10, 12, 18, 30 | finds 7092 |
. . . 4
⊢ (𝐵 ∈ ω → ((𝑈‘𝑎)‘𝐵) ⊆ (TC‘𝑎)) |
32 | 14 | itunifn 9239 |
. . . . . . . 8
⊢ (𝑎 ∈ V → (𝑈‘𝑎) Fn ω) |
33 | | fndm 5990 |
. . . . . . . 8
⊢ ((𝑈‘𝑎) Fn ω → dom (𝑈‘𝑎) = ω) |
34 | 13, 32, 33 | mp2b 10 |
. . . . . . 7
⊢ dom
(𝑈‘𝑎) = ω |
35 | 34 | eleq2i 2693 |
. . . . . 6
⊢ (𝐵 ∈ dom (𝑈‘𝑎) ↔ 𝐵 ∈ ω) |
36 | | ndmfv 6218 |
. . . . . 6
⊢ (¬
𝐵 ∈ dom (𝑈‘𝑎) → ((𝑈‘𝑎)‘𝐵) = ∅) |
37 | 35, 36 | sylnbir 321 |
. . . . 5
⊢ (¬
𝐵 ∈ ω →
((𝑈‘𝑎)‘𝐵) = ∅) |
38 | | 0ss 3972 |
. . . . 5
⊢ ∅
⊆ (TC‘𝑎) |
39 | 37, 38 | syl6eqss 3655 |
. . . 4
⊢ (¬
𝐵 ∈ ω →
((𝑈‘𝑎)‘𝐵) ⊆ (TC‘𝑎)) |
40 | 31, 39 | pm2.61i 176 |
. . 3
⊢ ((𝑈‘𝑎)‘𝐵) ⊆ (TC‘𝑎) |
41 | 4, 40 | vtoclg 3266 |
. 2
⊢ (𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) ⊆ (TC‘𝐴)) |
42 | | fvprc 6185 |
. . . . 5
⊢ (¬
𝐴 ∈ V → (𝑈‘𝐴) = ∅) |
43 | 42 | fveq1d 6193 |
. . . 4
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) = (∅‘𝐵)) |
44 | | 0fv 6227 |
. . . 4
⊢
(∅‘𝐵) =
∅ |
45 | 43, 44 | syl6eq 2672 |
. . 3
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) = ∅) |
46 | | 0ss 3972 |
. . 3
⊢ ∅
⊆ (TC‘𝐴) |
47 | 45, 46 | syl6eqss 3655 |
. 2
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) ⊆ (TC‘𝐴)) |
48 | 41, 47 | pm2.61i 176 |
1
⊢ ((𝑈‘𝐴)‘𝐵) ⊆ (TC‘𝐴) |