| Step | Hyp | Ref
| Expression |
| 1 | | wuncval2.f |
. . . 4
⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾
ω) |
| 2 | | wuncval2.u |
. . . 4
⊢ 𝑈 = ∪
ran 𝐹 |
| 3 | 1, 2 | wunex2 10778 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈)) |
| 4 | | wuncss 10785 |
. . 3
⊢ ((𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈) → (wUniCl‘𝐴) ⊆ 𝑈) |
| 5 | 3, 4 | syl 17 |
. 2
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) ⊆ 𝑈) |
| 6 | | frfnom 8475 |
. . . . . 6
⊢
(rec((𝑧 ∈ V
↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) Fn
ω |
| 7 | 1 | fneq1i 6665 |
. . . . . 6
⊢ (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾ ω) Fn
ω) |
| 8 | 6, 7 | mpbir 231 |
. . . . 5
⊢ 𝐹 Fn ω |
| 9 | | fniunfv 7267 |
. . . . 5
⊢ (𝐹 Fn ω → ∪ 𝑚 ∈ ω (𝐹‘𝑚) = ∪ ran 𝐹) |
| 10 | 8, 9 | ax-mp 5 |
. . . 4
⊢ ∪ 𝑚 ∈ ω (𝐹‘𝑚) = ∪ ran 𝐹 |
| 11 | 2, 10 | eqtr4i 2768 |
. . 3
⊢ 𝑈 = ∪ 𝑚 ∈ ω (𝐹‘𝑚) |
| 12 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑚 = ∅ → (𝐹‘𝑚) = (𝐹‘∅)) |
| 13 | 12 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑚 = ∅ → ((𝐹‘𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹‘∅) ⊆ (wUniCl‘𝐴))) |
| 14 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
| 15 | 14 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴))) |
| 16 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑚 = suc 𝑛 → (𝐹‘𝑚) = (𝐹‘suc 𝑛)) |
| 17 | 16 | sseq1d 4015 |
. . . . . . 7
⊢ (𝑚 = suc 𝑛 → ((𝐹‘𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴))) |
| 18 | | 1on 8518 |
. . . . . . . . . 10
⊢
1o ∈ On |
| 19 | | unexg 7763 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 1o ∈ On) →
(𝐴 ∪ 1o)
∈ V) |
| 20 | 18, 19 | mpan2 691 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1o) ∈
V) |
| 21 | 1 | fveq1i 6907 |
. . . . . . . . . 10
⊢ (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾
ω)‘∅) |
| 22 | | fr0g 8476 |
. . . . . . . . . 10
⊢ ((𝐴 ∪ 1o) ∈ V
→ ((rec((𝑧 ∈ V
↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1o)) ↾
ω)‘∅) = (𝐴 ∪ 1o)) |
| 23 | 21, 22 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝐴 ∪ 1o) ∈ V
→ (𝐹‘∅) =
(𝐴 ∪
1o)) |
| 24 | 20, 23 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝐹‘∅) = (𝐴 ∪ 1o)) |
| 25 | | wuncid 10783 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (wUniCl‘𝐴)) |
| 26 | | df1o2 8513 |
. . . . . . . . . 10
⊢
1o = {∅} |
| 27 | | wunccl 10784 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) ∈ WUni) |
| 28 | 27 | wun0 10758 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → ∅ ∈ (wUniCl‘𝐴)) |
| 29 | 28 | snssd 4809 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → {∅} ⊆
(wUniCl‘𝐴)) |
| 30 | 26, 29 | eqsstrid 4022 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 1o ⊆
(wUniCl‘𝐴)) |
| 31 | 25, 30 | unssd 4192 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1o) ⊆
(wUniCl‘𝐴)) |
| 32 | 24, 31 | eqsstrd 4018 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝐹‘∅) ⊆ (wUniCl‘𝐴)) |
| 33 | | simplr 769 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → 𝑛 ∈ ω) |
| 34 | | fvex 6919 |
. . . . . . . . . . . . 13
⊢ (𝐹‘𝑛) ∈ V |
| 35 | 34 | uniex 7761 |
. . . . . . . . . . . . 13
⊢ ∪ (𝐹‘𝑛) ∈ V |
| 36 | 34, 35 | unex 7764 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∈ V |
| 37 | | prex 5437 |
. . . . . . . . . . . . . 14
⊢
{𝒫 𝑢, ∪ 𝑢}
∈ V |
| 38 | 34 | mptex 7243 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}) ∈ V |
| 39 | 38 | rnex 7932 |
. . . . . . . . . . . . . 14
⊢ ran
(𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}) ∈ V |
| 40 | 37, 39 | unex 7764 |
. . . . . . . . . . . . 13
⊢
({𝒫 𝑢, ∪ 𝑢}
∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ∈ V |
| 41 | 34, 40 | iunex 7993 |
. . . . . . . . . . . 12
⊢ ∪ 𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ∈ V |
| 42 | 36, 41 | unex 7764 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}))) ∈ V |
| 43 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧) |
| 44 | | unieq 4918 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑧 → ∪ 𝑤 = ∪
𝑧) |
| 45 | 43, 44 | uneq12d 4169 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → (𝑤 ∪ ∪ 𝑤) = (𝑧 ∪ ∪ 𝑧)) |
| 46 | | pweq 4614 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥) |
| 47 | | unieq 4918 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑥 → ∪ 𝑢 = ∪
𝑥) |
| 48 | 46, 47 | preq12d 4741 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑥 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑥, ∪
𝑥}) |
| 49 | | preq1 4733 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑥 → {𝑢, 𝑣} = {𝑥, 𝑣}) |
| 50 | 49 | mpteq2dv 5244 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑥 → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣})) |
| 51 | 50 | rneqd 5949 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑥 → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣})) |
| 52 | 48, 51 | uneq12d 4169 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑥 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣}))) |
| 53 | 52 | cbviunv 5040 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪
𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣})) |
| 54 | | preq2 4734 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑦 → {𝑥, 𝑣} = {𝑥, 𝑦}) |
| 55 | 54 | cbvmptv 5255 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) |
| 56 | | mpteq1 5235 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})) |
| 57 | 55, 56 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑧 → (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣}) = (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})) |
| 58 | 57 | rneqd 5949 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑧 → ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣}) = ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})) |
| 59 | 58 | uneq2d 4168 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑧 → ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))) |
| 60 | 43, 59 | iuneq12d 5021 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑧 → ∪
𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣})) = ∪
𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))) |
| 61 | 53, 60 | eqtrid 2789 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → ∪
𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪
𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))) |
| 62 | 45, 61 | uneq12d 4169 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))) |
| 63 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐹‘𝑛) → 𝑤 = (𝐹‘𝑛)) |
| 64 | | unieq 4918 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐹‘𝑛) → ∪ 𝑤 = ∪
(𝐹‘𝑛)) |
| 65 | 63, 64 | uneq12d 4169 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐹‘𝑛) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛))) |
| 66 | | mpteq1 5235 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝐹‘𝑛) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) |
| 67 | 66 | rneqd 5949 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝐹‘𝑛) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) |
| 68 | 67 | uneq2d 4168 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐹‘𝑛) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}))) |
| 69 | 63, 68 | iuneq12d 5021 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐹‘𝑛) → ∪
𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}))) |
| 70 | 65, 69 | uneq12d 4169 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝐹‘𝑛) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})))) |
| 71 | 1, 62, 70 | frsucmpt2 8480 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ω ∧ (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑛) = (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})))) |
| 72 | 33, 42, 71 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹‘suc 𝑛) = (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})))) |
| 73 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) |
| 74 | 27 | ad3antrrr 730 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → (wUniCl‘𝐴) ∈ WUni) |
| 75 | 73 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → 𝑢 ∈ (wUniCl‘𝐴)) |
| 76 | 74, 75 | wunelss 10748 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → 𝑢 ⊆ (wUniCl‘𝐴)) |
| 77 | 76 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → ∀𝑢 ∈ (𝐹‘𝑛)𝑢 ⊆ (wUniCl‘𝐴)) |
| 78 | | unissb 4939 |
. . . . . . . . . . . . 13
⊢ (∪ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴) ↔ ∀𝑢 ∈ (𝐹‘𝑛)𝑢 ⊆ (wUniCl‘𝐴)) |
| 79 | 77, 78 | sylibr 234 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → ∪
(𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) |
| 80 | 73, 79 | unssd 4192 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → ((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ⊆ (wUniCl‘𝐴)) |
| 81 | 74, 75 | wunpw 10747 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → 𝒫 𝑢 ∈ (wUniCl‘𝐴)) |
| 82 | 74, 75 | wununi 10746 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → ∪ 𝑢 ∈ (wUniCl‘𝐴)) |
| 83 | 81, 82 | prssd 4822 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → {𝒫 𝑢, ∪ 𝑢} ⊆ (wUniCl‘𝐴)) |
| 84 | 74 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) ∧ 𝑣 ∈ (𝐹‘𝑛)) → (wUniCl‘𝐴) ∈ WUni) |
| 85 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) ∧ 𝑣 ∈ (𝐹‘𝑛)) → 𝑢 ∈ (wUniCl‘𝐴)) |
| 86 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) |
| 87 | 86 | sselda 3983 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) ∧ 𝑣 ∈ (𝐹‘𝑛)) → 𝑣 ∈ (wUniCl‘𝐴)) |
| 88 | 84, 85, 87 | wunpr 10749 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) ∧ 𝑣 ∈ (𝐹‘𝑛)) → {𝑢, 𝑣} ∈ (wUniCl‘𝐴)) |
| 89 | 88 | fmpttd 7135 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}):(𝐹‘𝑛)⟶(wUniCl‘𝐴)) |
| 90 | 89 | frnd 6744 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}) ⊆ (wUniCl‘𝐴)) |
| 91 | 83, 90 | unssd 4192 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴)) |
| 92 | 91 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → ∀𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴)) |
| 93 | | iunss 5045 |
. . . . . . . . . . . 12
⊢ (∪ 𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴) ↔ ∀𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴)) |
| 94 | 92, 93 | sylibr 234 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → ∪ 𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴)) |
| 95 | 80, 94 | unssd 4192 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}))) ⊆ (wUniCl‘𝐴)) |
| 96 | 72, 95 | eqsstrd 4018 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴)) |
| 97 | 96 | ex 412 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) → ((𝐹‘𝑛) ⊆ (wUniCl‘𝐴) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴))) |
| 98 | 97 | expcom 413 |
. . . . . . 7
⊢ (𝑛 ∈ ω → (𝐴 ∈ 𝑉 → ((𝐹‘𝑛) ⊆ (wUniCl‘𝐴) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴)))) |
| 99 | 13, 15, 17, 32, 98 | finds2 7920 |
. . . . . 6
⊢ (𝑚 ∈ ω → (𝐴 ∈ 𝑉 → (𝐹‘𝑚) ⊆ (wUniCl‘𝐴))) |
| 100 | 99 | com12 32 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (wUniCl‘𝐴))) |
| 101 | 100 | ralrimiv 3145 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∀𝑚 ∈ ω (𝐹‘𝑚) ⊆ (wUniCl‘𝐴)) |
| 102 | | iunss 5045 |
. . . 4
⊢ (∪ 𝑚 ∈ ω (𝐹‘𝑚) ⊆ (wUniCl‘𝐴) ↔ ∀𝑚 ∈ ω (𝐹‘𝑚) ⊆ (wUniCl‘𝐴)) |
| 103 | 101, 102 | sylibr 234 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∪
𝑚 ∈ ω (𝐹‘𝑚) ⊆ (wUniCl‘𝐴)) |
| 104 | 11, 103 | eqsstrid 4022 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝑈 ⊆ (wUniCl‘𝐴)) |
| 105 | 5, 104 | eqssd 4001 |
1
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) = 𝑈) |