Step | Hyp | Ref
| Expression |
1 | | wuncval2.f |
. . . 4
⊢ 𝐹 = (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾
ω) |
2 | | wuncval2.u |
. . . 4
⊢ 𝑈 = ∪
ran 𝐹 |
3 | 1, 2 | wunex2 9439 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈)) |
4 | | wuncss 9446 |
. . 3
⊢ ((𝑈 ∈ WUni ∧ 𝐴 ⊆ 𝑈) → (wUniCl‘𝐴) ⊆ 𝑈) |
5 | 3, 4 | syl 17 |
. 2
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) ⊆ 𝑈) |
6 | | frfnom 7417 |
. . . . . 6
⊢
(rec((𝑧 ∈ V
↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾
ω) Fn ω |
7 | 1 | fneq1i 5899 |
. . . . . 6
⊢ (𝐹 Fn ω ↔ (rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾
ω) Fn ω) |
8 | 6, 7 | mpbir 220 |
. . . . 5
⊢ 𝐹 Fn ω |
9 | | fniunfv 6409 |
. . . . 5
⊢ (𝐹 Fn ω → ∪ 𝑚 ∈ ω (𝐹‘𝑚) = ∪ ran 𝐹) |
10 | 8, 9 | ax-mp 5 |
. . . 4
⊢ ∪ 𝑚 ∈ ω (𝐹‘𝑚) = ∪ ran 𝐹 |
11 | 2, 10 | eqtr4i 2635 |
. . 3
⊢ 𝑈 = ∪ 𝑚 ∈ ω (𝐹‘𝑚) |
12 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = ∅ → (𝐹‘𝑚) = (𝐹‘∅)) |
13 | 12 | sseq1d 3595 |
. . . . . . 7
⊢ (𝑚 = ∅ → ((𝐹‘𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹‘∅) ⊆ (wUniCl‘𝐴))) |
14 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
15 | 14 | sseq1d 3595 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴))) |
16 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑚 = suc 𝑛 → (𝐹‘𝑚) = (𝐹‘suc 𝑛)) |
17 | 16 | sseq1d 3595 |
. . . . . . 7
⊢ (𝑚 = suc 𝑛 → ((𝐹‘𝑚) ⊆ (wUniCl‘𝐴) ↔ (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴))) |
18 | | 1on 7454 |
. . . . . . . . . 10
⊢
1𝑜 ∈ On |
19 | | unexg 6857 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 1𝑜 ∈ On)
→ (𝐴 ∪
1𝑜) ∈ V) |
20 | 18, 19 | mpan2 703 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1𝑜) ∈
V) |
21 | 1 | fveq1i 6104 |
. . . . . . . . . 10
⊢ (𝐹‘∅) = ((rec((𝑧 ∈ V ↦ ((𝑧 ∪ ∪ 𝑧)
∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾
ω)‘∅) |
22 | | fr0g 7418 |
. . . . . . . . . 10
⊢ ((𝐴 ∪ 1𝑜)
∈ V → ((rec((𝑧
∈ V ↦ ((𝑧 ∪
∪ 𝑧) ∪ ∪
𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))), (𝐴 ∪ 1𝑜)) ↾
ω)‘∅) = (𝐴 ∪
1𝑜)) |
23 | 21, 22 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝐴 ∪ 1𝑜)
∈ V → (𝐹‘∅) = (𝐴 ∪
1𝑜)) |
24 | 20, 23 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝐹‘∅) = (𝐴 ∪
1𝑜)) |
25 | | wuncid 9444 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 𝐴 ⊆ (wUniCl‘𝐴)) |
26 | | df1o2 7459 |
. . . . . . . . . 10
⊢
1𝑜 = {∅} |
27 | | wunccl 9445 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) ∈ WUni) |
28 | 27 | wun0 9419 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ 𝑉 → ∅ ∈ (wUniCl‘𝐴)) |
29 | 28 | snssd 4281 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑉 → {∅} ⊆
(wUniCl‘𝐴)) |
30 | 26, 29 | syl5eqss 3612 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝑉 → 1𝑜 ⊆
(wUniCl‘𝐴)) |
31 | 25, 30 | unssd 3751 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∪ 1𝑜) ⊆
(wUniCl‘𝐴)) |
32 | 24, 31 | eqsstrd 3602 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑉 → (𝐹‘∅) ⊆ (wUniCl‘𝐴)) |
33 | | simplr 788 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → 𝑛 ∈ ω) |
34 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐹‘𝑛) ∈ V |
35 | 34 | uniex 6851 |
. . . . . . . . . . . . 13
⊢ ∪ (𝐹‘𝑛) ∈ V |
36 | 34, 35 | unex 6854 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∈ V |
37 | | prex 4836 |
. . . . . . . . . . . . . 14
⊢
{𝒫 𝑢, ∪ 𝑢}
∈ V |
38 | 34 | mptex 6390 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}) ∈ V |
39 | 38 | rnex 6992 |
. . . . . . . . . . . . . 14
⊢ ran
(𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}) ∈ V |
40 | 37, 39 | unex 6854 |
. . . . . . . . . . . . 13
⊢
({𝒫 𝑢, ∪ 𝑢}
∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ∈ V |
41 | 34, 40 | iunex 7039 |
. . . . . . . . . . . 12
⊢ ∪ 𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ∈ V |
42 | 36, 41 | unex 6854 |
. . . . . . . . . . 11
⊢ (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}))) ∈ V |
43 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑧 → 𝑤 = 𝑧) |
44 | | unieq 4380 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑧 → ∪ 𝑤 = ∪
𝑧) |
45 | 43, 44 | uneq12d 3730 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → (𝑤 ∪ ∪ 𝑤) = (𝑧 ∪ ∪ 𝑧)) |
46 | | pweq 4111 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑥 → 𝒫 𝑢 = 𝒫 𝑥) |
47 | | unieq 4380 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑥 → ∪ 𝑢 = ∪
𝑥) |
48 | 46, 47 | preq12d 4220 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑥 → {𝒫 𝑢, ∪ 𝑢} = {𝒫 𝑥, ∪
𝑥}) |
49 | | preq1 4212 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑢 = 𝑥 → {𝑢, 𝑣} = {𝑥, 𝑣}) |
50 | 49 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑥 → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣})) |
51 | 50 | rneqd 5274 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑥 → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣})) |
52 | 48, 51 | uneq12d 3730 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑥 → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣}))) |
53 | 52 | cbviunv 4495 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪
𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣})) |
54 | | preq2 4213 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑦 → {𝑥, 𝑣} = {𝑥, 𝑦}) |
55 | 54 | cbvmptv 4678 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣}) = (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) |
56 | | mpteq1 4665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 = 𝑧 → (𝑦 ∈ 𝑤 ↦ {𝑥, 𝑦}) = (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})) |
57 | 55, 56 | syl5eq 2656 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑧 → (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣}) = (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})) |
58 | 57 | rneqd 5274 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 𝑧 → ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣}) = ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})) |
59 | 58 | uneq2d 3729 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 𝑧 → ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣})) = ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))) |
60 | 43, 59 | iuneq12d 4482 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 𝑧 → ∪
𝑥 ∈ 𝑤 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑥, 𝑣})) = ∪
𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))) |
61 | 53, 60 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 𝑧 → ∪
𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪
𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦}))) |
62 | 45, 61 | uneq12d 3730 |
. . . . . . . . . . . 12
⊢ (𝑤 = 𝑧 → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = ((𝑧 ∪ ∪ 𝑧) ∪ ∪ 𝑥 ∈ 𝑧 ({𝒫 𝑥, ∪ 𝑥} ∪ ran (𝑦 ∈ 𝑧 ↦ {𝑥, 𝑦})))) |
63 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐹‘𝑛) → 𝑤 = (𝐹‘𝑛)) |
64 | | unieq 4380 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐹‘𝑛) → ∪ 𝑤 = ∪
(𝐹‘𝑛)) |
65 | 63, 64 | uneq12d 3730 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐹‘𝑛) → (𝑤 ∪ ∪ 𝑤) = ((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛))) |
66 | | mpteq1 4665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝐹‘𝑛) → (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) |
67 | 66 | rneqd 5274 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = (𝐹‘𝑛) → ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}) = ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) |
68 | 67 | uneq2d 3729 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = (𝐹‘𝑛) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}))) |
69 | 63, 68 | iuneq12d 4482 |
. . . . . . . . . . . . 13
⊢ (𝑤 = (𝐹‘𝑛) → ∪
𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣})) = ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}))) |
70 | 65, 69 | uneq12d 3730 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝐹‘𝑛) → ((𝑤 ∪ ∪ 𝑤) ∪ ∪ 𝑢 ∈ 𝑤 ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ 𝑤 ↦ {𝑢, 𝑣}))) = (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})))) |
71 | 1, 62, 70 | frsucmpt2 7422 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ω ∧ (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}))) ∈ V) → (𝐹‘suc 𝑛) = (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})))) |
72 | 33, 42, 71 | sylancl 693 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹‘suc 𝑛) = (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})))) |
73 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) |
74 | 27 | ad3antrrr 762 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → (wUniCl‘𝐴) ∈ WUni) |
75 | 73 | sselda 3568 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → 𝑢 ∈ (wUniCl‘𝐴)) |
76 | 74, 75 | wunelss 9409 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → 𝑢 ⊆ (wUniCl‘𝐴)) |
77 | 76 | ralrimiva 2949 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → ∀𝑢 ∈ (𝐹‘𝑛)𝑢 ⊆ (wUniCl‘𝐴)) |
78 | | unissb 4405 |
. . . . . . . . . . . . 13
⊢ (∪ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴) ↔ ∀𝑢 ∈ (𝐹‘𝑛)𝑢 ⊆ (wUniCl‘𝐴)) |
79 | 77, 78 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → ∪
(𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) |
80 | 73, 79 | unssd 3751 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → ((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ⊆ (wUniCl‘𝐴)) |
81 | 74, 75 | wunpw 9408 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → 𝒫 𝑢 ∈ (wUniCl‘𝐴)) |
82 | 74, 75 | wununi 9407 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → ∪ 𝑢 ∈ (wUniCl‘𝐴)) |
83 | | prssi 4293 |
. . . . . . . . . . . . . . 15
⊢
((𝒫 𝑢 ∈
(wUniCl‘𝐴) ∧
∪ 𝑢 ∈ (wUniCl‘𝐴)) → {𝒫 𝑢, ∪ 𝑢} ⊆ (wUniCl‘𝐴)) |
84 | 81, 82, 83 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → {𝒫 𝑢, ∪ 𝑢} ⊆ (wUniCl‘𝐴)) |
85 | 74 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) ∧ 𝑣 ∈ (𝐹‘𝑛)) → (wUniCl‘𝐴) ∈ WUni) |
86 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) ∧ 𝑣 ∈ (𝐹‘𝑛)) → 𝑢 ∈ (wUniCl‘𝐴)) |
87 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) |
88 | 87 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) ∧ 𝑣 ∈ (𝐹‘𝑛)) → 𝑣 ∈ (wUniCl‘𝐴)) |
89 | 85, 86, 88 | wunpr 9410 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) ∧ 𝑣 ∈ (𝐹‘𝑛)) → {𝑢, 𝑣} ∈ (wUniCl‘𝐴)) |
90 | | eqid 2610 |
. . . . . . . . . . . . . . . 16
⊢ (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}) = (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}) |
91 | 89, 90 | fmptd 6292 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}):(𝐹‘𝑛)⟶(wUniCl‘𝐴)) |
92 | | frn 5966 |
. . . . . . . . . . . . . . 15
⊢ ((𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}):(𝐹‘𝑛)⟶(wUniCl‘𝐴) → ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}) ⊆ (wUniCl‘𝐴)) |
93 | 91, 92 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}) ⊆ (wUniCl‘𝐴)) |
94 | 84, 93 | unssd 3751 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) ∧ 𝑢 ∈ (𝐹‘𝑛)) → ({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴)) |
95 | 94 | ralrimiva 2949 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → ∀𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴)) |
96 | | iunss 4497 |
. . . . . . . . . . . 12
⊢ (∪ 𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴) ↔ ∀𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴)) |
97 | 95, 96 | sylibr 223 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → ∪ 𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣})) ⊆ (wUniCl‘𝐴)) |
98 | 80, 97 | unssd 3751 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → (((𝐹‘𝑛) ∪ ∪ (𝐹‘𝑛)) ∪ ∪
𝑢 ∈ (𝐹‘𝑛)({𝒫 𝑢, ∪ 𝑢} ∪ ran (𝑣 ∈ (𝐹‘𝑛) ↦ {𝑢, 𝑣}))) ⊆ (wUniCl‘𝐴)) |
99 | 72, 98 | eqsstrd 3602 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) ∧ (𝐹‘𝑛) ⊆ (wUniCl‘𝐴)) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴)) |
100 | 99 | ex 449 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑛 ∈ ω) → ((𝐹‘𝑛) ⊆ (wUniCl‘𝐴) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴))) |
101 | 100 | expcom 450 |
. . . . . . 7
⊢ (𝑛 ∈ ω → (𝐴 ∈ 𝑉 → ((𝐹‘𝑛) ⊆ (wUniCl‘𝐴) → (𝐹‘suc 𝑛) ⊆ (wUniCl‘𝐴)))) |
102 | 13, 15, 17, 32, 101 | finds2 6986 |
. . . . . 6
⊢ (𝑚 ∈ ω → (𝐴 ∈ 𝑉 → (𝐹‘𝑚) ⊆ (wUniCl‘𝐴))) |
103 | 102 | com12 32 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝑚 ∈ ω → (𝐹‘𝑚) ⊆ (wUniCl‘𝐴))) |
104 | 103 | ralrimiv 2948 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → ∀𝑚 ∈ ω (𝐹‘𝑚) ⊆ (wUniCl‘𝐴)) |
105 | | iunss 4497 |
. . . 4
⊢ (∪ 𝑚 ∈ ω (𝐹‘𝑚) ⊆ (wUniCl‘𝐴) ↔ ∀𝑚 ∈ ω (𝐹‘𝑚) ⊆ (wUniCl‘𝐴)) |
106 | 104, 105 | sylibr 223 |
. . 3
⊢ (𝐴 ∈ 𝑉 → ∪
𝑚 ∈ ω (𝐹‘𝑚) ⊆ (wUniCl‘𝐴)) |
107 | 11, 106 | syl5eqss 3612 |
. 2
⊢ (𝐴 ∈ 𝑉 → 𝑈 ⊆ (wUniCl‘𝐴)) |
108 | 5, 107 | eqssd 3585 |
1
⊢ (𝐴 ∈ 𝑉 → (wUniCl‘𝐴) = 𝑈) |