| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . 5
⊢ (𝑎 = 𝐴 → (𝑈‘𝑎) = (𝑈‘𝐴)) |
| 2 | 1 | fveq1d 6908 |
. . . 4
⊢ (𝑎 = 𝐴 → ((𝑈‘𝑎)‘𝐵) = ((𝑈‘𝐴)‘𝐵)) |
| 3 | | fveq2 6906 |
. . . 4
⊢ (𝑎 = 𝐴 → (TC‘𝑎) = (TC‘𝐴)) |
| 4 | 2, 3 | sseq12d 4017 |
. . 3
⊢ (𝑎 = 𝐴 → (((𝑈‘𝑎)‘𝐵) ⊆ (TC‘𝑎) ↔ ((𝑈‘𝐴)‘𝐵) ⊆ (TC‘𝐴))) |
| 5 | | fveq2 6906 |
. . . . . 6
⊢ (𝑏 = ∅ → ((𝑈‘𝑎)‘𝑏) = ((𝑈‘𝑎)‘∅)) |
| 6 | 5 | sseq1d 4015 |
. . . . 5
⊢ (𝑏 = ∅ → (((𝑈‘𝑎)‘𝑏) ⊆ (TC‘𝑎) ↔ ((𝑈‘𝑎)‘∅) ⊆ (TC‘𝑎))) |
| 7 | | fveq2 6906 |
. . . . . 6
⊢ (𝑏 = 𝑐 → ((𝑈‘𝑎)‘𝑏) = ((𝑈‘𝑎)‘𝑐)) |
| 8 | 7 | sseq1d 4015 |
. . . . 5
⊢ (𝑏 = 𝑐 → (((𝑈‘𝑎)‘𝑏) ⊆ (TC‘𝑎) ↔ ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎))) |
| 9 | | fveq2 6906 |
. . . . . 6
⊢ (𝑏 = suc 𝑐 → ((𝑈‘𝑎)‘𝑏) = ((𝑈‘𝑎)‘suc 𝑐)) |
| 10 | 9 | sseq1d 4015 |
. . . . 5
⊢ (𝑏 = suc 𝑐 → (((𝑈‘𝑎)‘𝑏) ⊆ (TC‘𝑎) ↔ ((𝑈‘𝑎)‘suc 𝑐) ⊆ (TC‘𝑎))) |
| 11 | | fveq2 6906 |
. . . . . 6
⊢ (𝑏 = 𝐵 → ((𝑈‘𝑎)‘𝑏) = ((𝑈‘𝑎)‘𝐵)) |
| 12 | 11 | sseq1d 4015 |
. . . . 5
⊢ (𝑏 = 𝐵 → (((𝑈‘𝑎)‘𝑏) ⊆ (TC‘𝑎) ↔ ((𝑈‘𝑎)‘𝐵) ⊆ (TC‘𝑎))) |
| 13 | | ituni.u |
. . . . . . . 8
⊢ 𝑈 = (𝑥 ∈ V ↦ (rec((𝑦 ∈ V ↦ ∪ 𝑦),
𝑥) ↾
ω)) |
| 14 | 13 | ituni0 10458 |
. . . . . . 7
⊢ (𝑎 ∈ V → ((𝑈‘𝑎)‘∅) = 𝑎) |
| 15 | | tcid 9779 |
. . . . . . 7
⊢ (𝑎 ∈ V → 𝑎 ⊆ (TC‘𝑎)) |
| 16 | 14, 15 | eqsstrd 4018 |
. . . . . 6
⊢ (𝑎 ∈ V → ((𝑈‘𝑎)‘∅) ⊆ (TC‘𝑎)) |
| 17 | 16 | elv 3485 |
. . . . 5
⊢ ((𝑈‘𝑎)‘∅) ⊆ (TC‘𝑎) |
| 18 | 13 | itunisuc 10459 |
. . . . . . 7
⊢ ((𝑈‘𝑎)‘suc 𝑐) = ∪ ((𝑈‘𝑎)‘𝑐) |
| 19 | | tctr 9780 |
. . . . . . . . . 10
⊢ Tr
(TC‘𝑎) |
| 20 | | pwtr 5457 |
. . . . . . . . . 10
⊢ (Tr
(TC‘𝑎) ↔ Tr
𝒫 (TC‘𝑎)) |
| 21 | 19, 20 | mpbi 230 |
. . . . . . . . 9
⊢ Tr
𝒫 (TC‘𝑎) |
| 22 | | trss 5270 |
. . . . . . . . 9
⊢ (Tr
𝒫 (TC‘𝑎)
→ (((𝑈‘𝑎)‘𝑐) ∈ 𝒫 (TC‘𝑎) → ((𝑈‘𝑎)‘𝑐) ⊆ 𝒫 (TC‘𝑎))) |
| 23 | 21, 22 | ax-mp 5 |
. . . . . . . 8
⊢ (((𝑈‘𝑎)‘𝑐) ∈ 𝒫 (TC‘𝑎) → ((𝑈‘𝑎)‘𝑐) ⊆ 𝒫 (TC‘𝑎)) |
| 24 | | fvex 6919 |
. . . . . . . . 9
⊢ ((𝑈‘𝑎)‘𝑐) ∈ V |
| 25 | 24 | elpw 4604 |
. . . . . . . 8
⊢ (((𝑈‘𝑎)‘𝑐) ∈ 𝒫 (TC‘𝑎) ↔ ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎)) |
| 26 | | sspwuni 5100 |
. . . . . . . 8
⊢ (((𝑈‘𝑎)‘𝑐) ⊆ 𝒫 (TC‘𝑎) ↔ ∪ ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎)) |
| 27 | 23, 25, 26 | 3imtr3i 291 |
. . . . . . 7
⊢ (((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎) → ∪ ((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎)) |
| 28 | 18, 27 | eqsstrid 4022 |
. . . . . 6
⊢ (((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎) → ((𝑈‘𝑎)‘suc 𝑐) ⊆ (TC‘𝑎)) |
| 29 | 28 | a1i 11 |
. . . . 5
⊢ (𝑐 ∈ ω → (((𝑈‘𝑎)‘𝑐) ⊆ (TC‘𝑎) → ((𝑈‘𝑎)‘suc 𝑐) ⊆ (TC‘𝑎))) |
| 30 | 6, 8, 10, 12, 17, 29 | finds 7918 |
. . . 4
⊢ (𝐵 ∈ ω → ((𝑈‘𝑎)‘𝐵) ⊆ (TC‘𝑎)) |
| 31 | | vex 3484 |
. . . . . . . 8
⊢ 𝑎 ∈ V |
| 32 | 13 | itunifn 10457 |
. . . . . . . 8
⊢ (𝑎 ∈ V → (𝑈‘𝑎) Fn ω) |
| 33 | | fndm 6671 |
. . . . . . . 8
⊢ ((𝑈‘𝑎) Fn ω → dom (𝑈‘𝑎) = ω) |
| 34 | 31, 32, 33 | mp2b 10 |
. . . . . . 7
⊢ dom
(𝑈‘𝑎) = ω |
| 35 | 34 | eleq2i 2833 |
. . . . . 6
⊢ (𝐵 ∈ dom (𝑈‘𝑎) ↔ 𝐵 ∈ ω) |
| 36 | | ndmfv 6941 |
. . . . . 6
⊢ (¬
𝐵 ∈ dom (𝑈‘𝑎) → ((𝑈‘𝑎)‘𝐵) = ∅) |
| 37 | 35, 36 | sylnbir 331 |
. . . . 5
⊢ (¬
𝐵 ∈ ω →
((𝑈‘𝑎)‘𝐵) = ∅) |
| 38 | | 0ss 4400 |
. . . . 5
⊢ ∅
⊆ (TC‘𝑎) |
| 39 | 37, 38 | eqsstrdi 4028 |
. . . 4
⊢ (¬
𝐵 ∈ ω →
((𝑈‘𝑎)‘𝐵) ⊆ (TC‘𝑎)) |
| 40 | 30, 39 | pm2.61i 182 |
. . 3
⊢ ((𝑈‘𝑎)‘𝐵) ⊆ (TC‘𝑎) |
| 41 | 4, 40 | vtoclg 3554 |
. 2
⊢ (𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) ⊆ (TC‘𝐴)) |
| 42 | | fv2prc 6951 |
. . 3
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) = ∅) |
| 43 | | 0ss 4400 |
. . 3
⊢ ∅
⊆ (TC‘𝐴) |
| 44 | 42, 43 | eqsstrdi 4028 |
. 2
⊢ (¬
𝐴 ∈ V → ((𝑈‘𝐴)‘𝐵) ⊆ (TC‘𝐴)) |
| 45 | 41, 44 | pm2.61i 182 |
1
⊢ ((𝑈‘𝐴)‘𝐵) ⊆ (TC‘𝐴) |