| Step | Hyp | Ref
| Expression |
| 1 | | wunex2.u |
. . . . . . . 8
⊢ 𝑈 = ∪
ran 𝐹 |
| 2 | 1 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑎 ∈ 𝑈 ↔ 𝑎 ∈ ∪ ran
𝐹) |
| 3 | | frfnom 8475 |
. . . . . . . . 9
⊢
(rec((𝑧 ∈ V
↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) Fn
ω |
| 4 | | wunex2.f |
. . . . . . . . . 10
⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾
ω) |
| 5 | 4 | fneq1i 6665 |
. . . . . . . . 9
⊢ (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) Fn
ω) |
| 6 | 3, 5 | mpbir 231 |
. . . . . . . 8
⊢ 𝐹 Fn ω |
| 7 | | fnunirn 7274 |
. . . . . . . 8
⊢ (𝐹 Fn ω → (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚))) |
| 8 | 6, 7 | ax-mp 5 |
. . . . . . 7
⊢ (𝑎 ∈ ∪ ran 𝐹 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚)) |
| 9 | 2, 8 | bitri 275 |
. . . . . 6
⊢ (𝑎 ∈ 𝑈 ↔ ∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚)) |
| 10 | | elssuni 4937 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ ∪ (𝐹‘𝑚)) |
| 11 | 10 | ad2antll 729 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ ∪ (𝐹‘𝑚)) |
| 12 | | ssun2 4179 |
. . . . . . . . . . 11
⊢ ∪ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) |
| 13 | | ssun1 4178 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) |
| 14 | 12, 13 | sstri 3993 |
. . . . . . . . . 10
⊢ ∪ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) |
| 15 | 11, 14 | sstrdi 3996 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))) |
| 16 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑚 ∈ ω) |
| 17 | | fvex 6919 |
. . . . . . . . . . . 12
⊢ (𝐹‘𝑚) ∈ V |
| 18 | 17 | uniex 7761 |
. . . . . . . . . . . 12
⊢ ∪ (𝐹‘𝑚) ∈ V |
| 19 | 17, 18 | unex 7764 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∈ V |
| 20 | | prex 5437 |
. . . . . . . . . . . . 13
⊢
{𝒫 𝑢, ∪ 𝑢}
∈ V |
| 21 | 17 | mptex 7243 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V |
| 22 | 21 | rnex 7932 |
. . . . . . . . . . . . 13
⊢ ran
(𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) ∈ V |
| 23 | 20, 22 | unex 7764 |
. . . . . . . . . . . 12
⊢
({𝒫 𝑢, ∪ 𝑢}
∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V |
| 24 | 17, 23 | iunex 7993 |
. . . . . . . . . . 11
⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ∈ V |
| 25 | 19, 24 | unex 7764 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V |
| 26 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧) |
| 27 | | unieq 4918 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → ∪ 𝑤 = ∪
𝑧) |
| 28 | 26, 27 | uneq12d 4169 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → (𝑤 ∪ ∪ 𝑤) = (𝑧 ∪ ∪ 𝑧)) |
| 29 | | pweq 4614 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥) |
| 30 | | unieq 4918 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑥 → ∪ 𝑢 = ∪
𝑥) |
| 31 | 29, 30 | preq12d 4741 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑥 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑥, ∪
𝑥}) |
| 32 | | preq2 4734 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑦 → {𝑢, 𝑣} = {𝑢, 𝑦}) |
| 33 | 32 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦}) |
| 34 | | preq1 4733 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑥 → {𝑢, 𝑦} = {𝑥, 𝑦}) |
| 35 | 34 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑥 → (𝑦 ∈ 𝑤 ↦ {𝑢, 𝑦}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) |
| 36 | 33, 35 | eqtrid 2789 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑥 → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) |
| 37 | 36 | rneqd 5949 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑥 → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) |
| 38 | 31, 37 | uneq12d 4169 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑥 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}))) |
| 39 | 38 | cbviunv 5040 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪
𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) |
| 40 | | mpteq1 5235 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑧 → (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})) |
| 41 | 40 | rneqd 5949 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑧 → ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})) |
| 42 | 41 | uneq2d 4168 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑧 → ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))) |
| 43 | 26, 42 | iuneq12d 5021 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → ∪
𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦})) = ∪
𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))) |
| 44 | 39, 43 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → ∪
𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪
𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))) |
| 45 | 28, 44 | uneq12d 4169 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑧 → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))) |
| 46 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐹‘𝑚) → 𝑤 = (𝐹‘𝑚)) |
| 47 | | unieq 4918 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐹‘𝑚) → ∪ 𝑤 = ∪
(𝐹‘𝑚)) |
| 48 | 46, 47 | uneq12d 4169 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝐹‘𝑚) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚))) |
| 49 | | mpteq1 5235 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝐹‘𝑚) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) |
| 50 | 49 | rneqd 5949 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐹‘𝑚) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) |
| 51 | 50 | uneq2d 4168 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐹‘𝑚) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) |
| 52 | 46, 51 | iuneq12d 5021 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝐹‘𝑚) → ∪
𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) |
| 53 | 48, 52 | uneq12d 4169 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝐹‘𝑚) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))) |
| 54 | 4, 45, 53 | frsucmpt2 8480 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ω ∧ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))) |
| 55 | 16, 25, 54 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))) |
| 56 | 15, 55 | sseqtrrd 4021 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ (𝐹‘suc 𝑚)) |
| 57 | | fvssunirn 6939 |
. . . . . . . . 9
⊢ (𝐹‘suc 𝑚) ⊆ ∪ ran
𝐹 |
| 58 | 57, 1 | sseqtrri 4033 |
. . . . . . . 8
⊢ (𝐹‘suc 𝑚) ⊆ 𝑈 |
| 59 | 56, 58 | sstrdi 3996 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝑎 ⊆ 𝑈) |
| 60 | 59 | rexlimdvaa 3156 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → 𝑎 ⊆ 𝑈)) |
| 61 | 9, 60 | biimtrid 242 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → 𝑎 ⊆ 𝑈)) |
| 62 | 61 | ralrimiv 3145 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈) |
| 63 | | dftr3 5265 |
. . . 4
⊢ (Tr 𝑈 ↔ ∀𝑎 ∈ 𝑈 𝑎 ⊆ 𝑈) |
| 64 | 62, 63 | sylibr 234 |
. . 3
⊢ (𝐴 ∈ 𝑉 → Tr 𝑈) |
| 65 | | 1on 8518 |
. . . . . . . 8
⊢
1o ∈ On |
| 66 | | unexg 7763 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 1o ∈ On) →
(𝐴 ∪ 1o)
∈ V) |
| 67 | 65, 66 | mpan2 691 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1o) ∈
V) |
| 68 | 4 | fveq1i 6907 |
. . . . . . . 8
⊢ (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾
ω)‘∅) |
| 69 | | fr0g 8476 |
. . . . . . . 8
⊢ ((𝐴 ∪ 1o) ∈ V
→ ((rec((𝑧 ∈ V
↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾
ω)‘∅) = (𝐴 ∪ 1o)) |
| 70 | 68, 69 | eqtrid 2789 |
. . . . . . 7
⊢ ((𝐴 ∪ 1o) ∈ V
→ (𝐹‘∅) =
(𝐴 ∪
1o)) |
| 71 | 67, 70 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝐹‘∅) = (𝐴 ∪ 1o)) |
| 72 | | fvssunirn 6939 |
. . . . . . 7
⊢ (𝐹‘∅) ⊆ ∪ ran 𝐹 |
| 73 | 72, 1 | sseqtrri 4033 |
. . . . . 6
⊢ (𝐹‘∅) ⊆ 𝑈 |
| 74 | 71, 73 | eqsstrrdi 4029 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1o) ⊆ 𝑈) |
| 75 | 74 | unssbd 4194 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → 1o ⊆ 𝑈) |
| 76 | | 1n0 8526 |
. . . 4
⊢
1o ≠ ∅ |
| 77 | | ssn0 4404 |
. . . 4
⊢
((1o ⊆ 𝑈 ∧ 1o ≠ ∅) →
𝑈 ≠
∅) |
| 78 | 75, 76, 77 | sylancl 586 |
. . 3
⊢ (𝐴 ∈ 𝑉 → 𝑈 ≠ ∅) |
| 79 | | pweq 4614 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑎 → 𝒫 𝑢 = 𝒫 𝑎) |
| 80 | | unieq 4918 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪
𝑎) |
| 81 | 79, 80 | preq12d 4741 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑎 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑎, ∪
𝑎}) |
| 82 | | preq1 4733 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑎 → {𝑢, 𝑣} = {𝑎, 𝑣}) |
| 83 | 82 | mpteq2dv 5244 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) |
| 84 | 83 | rneqd 5949 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) |
| 85 | 81, 84 | uneq12d 4169 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣}))) |
| 86 | 85 | ssiun2s 5048 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ (𝐹‘𝑚) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) |
| 87 | 86 | ad2antll 729 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) |
| 88 | | ssun2 4179 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) |
| 89 | 88, 55 | sseqtrrid 4027 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc 𝑚)) |
| 90 | 89, 58 | sstrdi 3996 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})) ⊆ 𝑈) |
| 91 | 87, 90 | sstrd 3994 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑎, 𝑣})) ⊆ 𝑈) |
| 92 | 91 | unssad 4193 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → {𝒫 𝑎, ∪ 𝑎} ⊆ 𝑈) |
| 93 | | vpwex 5377 |
. . . . . . . . . 10
⊢ 𝒫
𝑎 ∈ V |
| 94 | | vuniex 7759 |
. . . . . . . . . 10
⊢ ∪ 𝑎
∈ V |
| 95 | 93, 94 | prss 4820 |
. . . . . . . . 9
⊢
((𝒫 𝑎 ∈
𝑈 ∧ ∪ 𝑎
∈ 𝑈) ↔ {𝒫
𝑎, ∪ 𝑎}
⊆ 𝑈) |
| 96 | 92, 95 | sylibr 234 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝒫 𝑎 ∈ 𝑈 ∧ ∪ 𝑎 ∈ 𝑈)) |
| 97 | 96 | simprd 495 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∪ 𝑎 ∈ 𝑈) |
| 98 | 96 | simpld 494 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → 𝒫 𝑎 ∈ 𝑈) |
| 99 | 1 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝑈 ↔ 𝑏 ∈ ∪ ran
𝐹) |
| 100 | | fnunirn 7274 |
. . . . . . . . . . 11
⊢ (𝐹 Fn ω → (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛))) |
| 101 | 6, 100 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑏 ∈ ∪ ran 𝐹 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛)) |
| 102 | 99, 101 | bitri 275 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝑈 ↔ ∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛)) |
| 103 | | ordom 7897 |
. . . . . . . . . . . . . . . . 17
⊢ Ord
ω |
| 104 | | simplrl 777 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑚 ∈ ω) |
| 105 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑛 ∈ ω) |
| 106 | | ordunel 7847 |
. . . . . . . . . . . . . . . . 17
⊢ ((Ord
ω ∧ 𝑚 ∈
ω ∧ 𝑛 ∈
ω) → (𝑚 ∪
𝑛) ∈
ω) |
| 107 | 103, 104,
105, 106 | mp3an2i 1468 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝑚 ∪ 𝑛) ∈ ω) |
| 108 | | ssun1 4178 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑚 ⊆ (𝑚 ∪ 𝑛) |
| 109 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑚 → (𝐹‘𝑘) = (𝐹‘𝑚)) |
| 110 | 109 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑚 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑚))) |
| 111 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑖 → (𝐹‘𝑘) = (𝐹‘𝑖)) |
| 112 | 111 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘𝑖))) |
| 113 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = suc 𝑖 → (𝐹‘𝑘) = (𝐹‘suc 𝑖)) |
| 114 | 113 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = suc 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖))) |
| 115 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = (𝑚 ∪ 𝑛) → (𝐹‘𝑘) = (𝐹‘(𝑚 ∪ 𝑛))) |
| 116 | 115 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑘) ↔ (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))) |
| 117 | | ssidd 4007 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘𝑚)) |
| 118 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑖 → (𝐹‘𝑚) = (𝐹‘𝑖)) |
| 119 | | suceq 6450 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 = 𝑖 → suc 𝑚 = suc 𝑖) |
| 120 | 119 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 = 𝑖 → (𝐹‘suc 𝑚) = (𝐹‘suc 𝑖)) |
| 121 | 118, 120 | sseq12d 4017 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝑖 → ((𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚) ↔ (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖))) |
| 122 | | ssun1 4178 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐹‘𝑚) ⊆ ((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) |
| 123 | 122, 13 | sstri 3993 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹‘𝑚) ⊆ (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣}))) |
| 124 | 25, 54 | mpan2 691 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑚 ∈ ω → (𝐹‘suc 𝑚) = (((𝐹‘𝑚) ∪ ∪ (𝐹‘𝑚)) ∪ ∪
𝑢 ∈ (𝐹‘𝑚)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑚) ↦ {𝑢, 𝑣})))) |
| 125 | 123, 124 | sseqtrrid 4027 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑚)) |
| 126 | 121, 125 | vtoclga 3577 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ ω → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖)) |
| 127 | 126 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖)) |
| 128 | | sstr2 3990 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → ((𝐹‘𝑖) ⊆ (𝐹‘suc 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖))) |
| 129 | 127, 128 | syl5com 31 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘suc 𝑖))) |
| 130 | 110, 112,
114, 116, 117, 129 | findsg 7919 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ (𝑚 ∪ 𝑛)) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛))) |
| 131 | 108, 130 | mpan2 691 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ 𝑚 ∈ ω) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛))) |
| 132 | 107, 104,
131 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑚) ⊆ (𝐹‘(𝑚 ∪ 𝑛))) |
| 133 | | simplrr 778 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘𝑚)) |
| 134 | 132, 133 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛))) |
| 135 | 82 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑎 → (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) |
| 136 | 135 | rneqd 5949 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑎 → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) |
| 137 | 81, 136 | uneq12d 4169 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑎 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) = ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}))) |
| 138 | 137 | ssiun2s 5048 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) |
| 139 | 134, 138 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) |
| 140 | | ssun2 4179 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪
𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) |
| 141 | | fvex 6919 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V |
| 142 | 141 | uniex 7761 |
. . . . . . . . . . . . . . . . . 18
⊢ ∪ (𝐹‘(𝑚 ∪ 𝑛)) ∈ V |
| 143 | 141, 142 | unex 7764 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∈ V |
| 144 | 141 | mptex 7243 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V |
| 145 | 144 | rnex 7932 |
. . . . . . . . . . . . . . . . . . 19
⊢ ran
(𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}) ∈ V |
| 146 | 20, 145 | unex 7764 |
. . . . . . . . . . . . . . . . . 18
⊢
({𝒫 𝑢, ∪ 𝑢}
∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V |
| 147 | 141, 146 | iunex 7993 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ∈ V |
| 148 | 143, 147 | unex 7764 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪
𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V |
| 149 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → 𝑤 = (𝐹‘(𝑚 ∪ 𝑛))) |
| 150 | | unieq 4918 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪ 𝑤 = ∪
(𝐹‘(𝑚 ∪ 𝑛))) |
| 151 | 149, 150 | uneq12d 4169 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛)))) |
| 152 | | mpteq1 5235 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) |
| 153 | 152 | rneqd 5949 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) |
| 154 | 153 | uneq2d 4168 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) |
| 155 | 149, 154 | iuneq12d 5021 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ∪
𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪
𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) |
| 156 | 151, 155 | uneq12d 4169 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = (𝐹‘(𝑚 ∪ 𝑛)) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪
𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))) |
| 157 | 4, 45, 156 | frsucmpt2 8480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∪ 𝑛) ∈ ω ∧ (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪
𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪
𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))) |
| 158 | 107, 148,
157 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘suc (𝑚 ∪ 𝑛)) = (((𝐹‘(𝑚 ∪ 𝑛)) ∪ ∪ (𝐹‘(𝑚 ∪ 𝑛))) ∪ ∪
𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})))) |
| 159 | 140, 158 | sseqtrrid 4027 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ (𝐹‘suc (𝑚 ∪ 𝑛))) |
| 160 | | fvssunirn 6939 |
. . . . . . . . . . . . . . 15
⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ ∪ ran
𝐹 |
| 161 | 160, 1 | sseqtrri 4033 |
. . . . . . . . . . . . . 14
⊢ (𝐹‘suc (𝑚 ∪ 𝑛)) ⊆ 𝑈 |
| 162 | 159, 161 | sstrdi 3996 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ∪ 𝑢 ∈ (𝐹‘(𝑚 ∪ 𝑛))({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑢, 𝑣})) ⊆ 𝑈) |
| 163 | 139, 162 | sstrd 3994 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ({𝒫 𝑎, ∪ 𝑎} ∪ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) ⊆ 𝑈) |
| 164 | 163 | unssbd 4194 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) ⊆ 𝑈) |
| 165 | | ssun2 4179 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑛 ⊆ (𝑚 ∪ 𝑛) |
| 166 | | id 22 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑖 = (𝑚 ∪ 𝑛)) |
| 167 | 165, 166 | sseqtrrid 4027 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑖 = (𝑚 ∪ 𝑛) → 𝑛 ⊆ 𝑖) |
| 168 | 167 | biantrud 531 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝑛 ∈ ω ↔ (𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖))) |
| 169 | 168 | bicomd 223 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) ↔ 𝑛 ∈ ω)) |
| 170 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 = (𝑚 ∪ 𝑛) → (𝐹‘𝑖) = (𝐹‘(𝑚 ∪ 𝑛))) |
| 171 | 170 | sseq2d 4016 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 = (𝑚 ∪ 𝑛) → ((𝐹‘𝑛) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))) |
| 172 | 169, 171 | imbi12d 344 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 = (𝑚 ∪ 𝑛) → (((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)) ↔ (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))))) |
| 173 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝑛 → (𝑚 ∈ ω ↔ 𝑛 ∈ ω)) |
| 174 | 173 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑛 → ((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ↔ (𝑖 ∈ ω ∧ 𝑛 ∈ ω))) |
| 175 | | sseq1 4009 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑛 → (𝑚 ⊆ 𝑖 ↔ 𝑛 ⊆ 𝑖)) |
| 176 | 174, 175 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = 𝑛 → (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) ↔ ((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖))) |
| 177 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
| 178 | 177 | sseq1d 4015 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ⊆ (𝐹‘𝑖) ↔ (𝐹‘𝑛) ⊆ (𝐹‘𝑖))) |
| 179 | 176, 178 | imbi12d 344 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 𝑛 → ((((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖)) ↔ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)))) |
| 180 | 110, 112,
114, 112, 117, 129 | findsg 7919 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑖 ∈ ω ∧ 𝑚 ∈ ω) ∧ 𝑚 ⊆ 𝑖) → (𝐹‘𝑚) ⊆ (𝐹‘𝑖)) |
| 181 | 179, 180 | chvarvv 1998 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑖 ∈ ω ∧ 𝑛 ∈ ω) ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖)) |
| 182 | 181 | expl 457 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ ω → ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑖) → (𝐹‘𝑛) ⊆ (𝐹‘𝑖))) |
| 183 | 172, 182 | vtoclga 3577 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∪ 𝑛) ∈ ω → (𝑛 ∈ ω → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛)))) |
| 184 | 107, 105,
183 | sylc 65 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → (𝐹‘𝑛) ⊆ (𝐹‘(𝑚 ∪ 𝑛))) |
| 185 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘𝑛)) |
| 186 | 184, 185 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → 𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛))) |
| 187 | | prex 5437 |
. . . . . . . . . . . 12
⊢ {𝑎, 𝑏} ∈ V |
| 188 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) = (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣}) |
| 189 | | preq2 4734 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑏 → {𝑎, 𝑣} = {𝑎, 𝑏}) |
| 190 | 188, 189 | elrnmpt1s 5970 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ∧ {𝑎, 𝑏} ∈ V) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) |
| 191 | 186, 187,
190 | sylancl 586 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ ran (𝑣 ∈ (𝐹‘(𝑚 ∪ 𝑛)) ↦ {𝑎, 𝑣})) |
| 192 | 164, 191 | sseldd 3984 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) ∧ (𝑛 ∈ ω ∧ 𝑏 ∈ (𝐹‘𝑛))) → {𝑎, 𝑏} ∈ 𝑈) |
| 193 | 192 | rexlimdvaa 3156 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∃𝑛 ∈ ω 𝑏 ∈ (𝐹‘𝑛) → {𝑎, 𝑏} ∈ 𝑈)) |
| 194 | 102, 193 | biimtrid 242 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (𝑏 ∈ 𝑈 → {𝑎, 𝑏} ∈ 𝑈)) |
| 195 | 194 | ralrimiv 3145 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈) |
| 196 | 97, 98, 195 | 3jca 1129 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑚 ∈ ω ∧ 𝑎 ∈ (𝐹‘𝑚))) → (∪
𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)) |
| 197 | 196 | rexlimdvaa 3156 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (∃𝑚 ∈ ω 𝑎 ∈ (𝐹‘𝑚) → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))) |
| 198 | 9, 197 | biimtrid 242 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝑎 ∈ 𝑈 → (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))) |
| 199 | 198 | ralrimiv 3145 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)) |
| 200 | | rdgfun 8456 |
. . . . . . . . 9
⊢ Fun
rec((𝑧 ∈ V ↦
((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) |
| 201 | | omex 9683 |
. . . . . . . . 9
⊢ ω
∈ V |
| 202 | | resfunexg 7235 |
. . . . . . . . 9
⊢ ((Fun
rec((𝑧 ∈ V ↦
((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ∧ ω ∈
V) → (rec((𝑧 ∈ V
↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)
∈ V) |
| 203 | 200, 201,
202 | mp2an 692 |
. . . . . . . 8
⊢
(rec((𝑧 ∈ V
↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω)
∈ V |
| 204 | 4, 203 | eqeltri 2837 |
. . . . . . 7
⊢ 𝐹 ∈ V |
| 205 | 204 | rnex 7932 |
. . . . . 6
⊢ ran 𝐹 ∈ V |
| 206 | 205 | uniex 7761 |
. . . . 5
⊢ ∪ ran 𝐹 ∈ V |
| 207 | 1, 206 | eqeltri 2837 |
. . . 4
⊢ 𝑈 ∈ V |
| 208 | | iswun 10744 |
. . . 4
⊢ (𝑈 ∈ V → (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈)))) |
| 209 | 207, 208 | ax-mp 5 |
. . 3
⊢ (𝑈 ∈ WUni ↔ (Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀𝑎 ∈ 𝑈 (∪ 𝑎 ∈ 𝑈 ∧ 𝒫 𝑎 ∈ 𝑈 ∧ ∀𝑏 ∈ 𝑈 {𝑎, 𝑏} ∈ 𝑈))) |
| 210 | 64, 78, 199, 209 | syl3anbrc 1344 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝑈 ∈ WUni) |
| 211 | 74 | unssad 4193 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ 𝑈) |
| 212 | 210, 211 | jca 511 |
1
⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈)) |