Step | Hyp | Ref
| Expression |
1 | | ptcmp.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | ptcmp.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶Comp) |
3 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶Comp → 𝐹 Fn 𝐴) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐴) |
5 | | eqid 2610 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} |
6 | 5 | ptval 21183 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → (∏t‘𝐹) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
7 | 1, 4, 6 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 →
(∏t‘𝐹) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
8 | | cmptop 21008 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ Comp → 𝑥 ∈ Top) |
9 | 8 | ssriv 3572 |
. . . . . . . . . 10
⊢ Comp
⊆ Top |
10 | | fss 5969 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) →
𝐹:𝐴⟶Top) |
11 | 2, 9, 10 | sylancl 693 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶Top) |
12 | | ptcmp.2 |
. . . . . . . . . 10
⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) |
13 | 5, 12 | ptbasfi 21194 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))) |
14 | 1, 11, 13 | syl2anc 691 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))) |
15 | | uncom 3719 |
. . . . . . . . . 10
⊢ (ran
𝑆 ∪ {𝑋}) = ({𝑋} ∪ ran 𝑆) |
16 | | ptcmp.1 |
. . . . . . . . . . . 12
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) |
17 | 16 | rneqi 5273 |
. . . . . . . . . . 11
⊢ ran 𝑆 = ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) |
18 | 17 | uneq2i 3726 |
. . . . . . . . . 10
⊢ ({𝑋} ∪ ran 𝑆) = ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) |
19 | 15, 18 | eqtri 2632 |
. . . . . . . . 9
⊢ (ran
𝑆 ∪ {𝑋}) = ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) |
20 | 19 | fveq2i 6106 |
. . . . . . . 8
⊢
(fi‘(ran 𝑆
∪ {𝑋})) =
(fi‘({𝑋} ∪ ran
(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) |
21 | 14, 20 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘(ran 𝑆 ∪ {𝑋}))) |
22 | 21 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) |
23 | 7, 22 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 →
(∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) |
24 | 23 | unieqd 4382 |
. . . 4
⊢ (𝜑 → ∪ (∏t‘𝐹) = ∪
(topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) |
25 | | fibas 20592 |
. . . . 5
⊢
(fi‘(ran 𝑆
∪ {𝑋})) ∈
TopBases |
26 | | unitg 20582 |
. . . . 5
⊢
((fi‘(ran 𝑆
∪ {𝑋})) ∈ TopBases
→ ∪ (topGen‘(fi‘(ran 𝑆 ∪ {𝑋}))) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
27 | 25, 26 | ax-mp 5 |
. . . 4
⊢ ∪ (topGen‘(fi‘(ran 𝑆 ∪ {𝑋}))) = ∪
(fi‘(ran 𝑆 ∪
{𝑋})) |
28 | 24, 27 | syl6eq 2660 |
. . 3
⊢ (𝜑 → ∪ (∏t‘𝐹) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
29 | | eqid 2610 |
. . . . . 6
⊢
(∏t‘𝐹) = (∏t‘𝐹) |
30 | 29 | ptuni 21207 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = ∪
(∏t‘𝐹)) |
31 | 1, 11, 30 | syl2anc 691 |
. . . 4
⊢ (𝜑 → X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = ∪
(∏t‘𝐹)) |
32 | 12, 31 | syl5eq 2656 |
. . 3
⊢ (𝜑 → 𝑋 = ∪
(∏t‘𝐹)) |
33 | | ptcmp.5 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom
card)) |
34 | | pwexg 4776 |
. . . . . . 7
⊢ (𝑋 ∈ (UFL ∩ dom card)
→ 𝒫 𝑋 ∈
V) |
35 | 33, 34 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝑋 ∈ V) |
36 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) |
37 | 36 | mptpreima 5545 |
. . . . . . . . . . 11
⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑢} |
38 | | ssrab2 3650 |
. . . . . . . . . . 11
⊢ {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑢} ⊆ 𝑋 |
39 | 37, 38 | eqsstri 3598 |
. . . . . . . . . 10
⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋 |
40 | 33 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝑋 ∈ (UFL ∩ dom
card)) |
41 | | elpw2g 4754 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (UFL ∩ dom card)
→ ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋)) |
42 | 40, 41 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋)) |
43 | 39, 42 | mpbiri 247 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋) |
44 | 43 | ralrimivva 2954 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋) |
45 | 16 | fmpt2x 7125 |
. . . . . . . 8
⊢
(∀𝑘 ∈
𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ 𝑆:∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝒫 𝑋) |
46 | 44, 45 | sylib 207 |
. . . . . . 7
⊢ (𝜑 → 𝑆:∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝒫 𝑋) |
47 | | frn 5966 |
. . . . . . 7
⊢ (𝑆:∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝒫 𝑋 → ran 𝑆 ⊆ 𝒫 𝑋) |
48 | 46, 47 | syl 17 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝑋) |
49 | 35, 48 | ssexd 4733 |
. . . . 5
⊢ (𝜑 → ran 𝑆 ∈ V) |
50 | | snex 4835 |
. . . . 5
⊢ {𝑋} ∈ V |
51 | | unexg 6857 |
. . . . 5
⊢ ((ran
𝑆 ∈ V ∧ {𝑋} ∈ V) → (ran 𝑆 ∪ {𝑋}) ∈ V) |
52 | 49, 50, 51 | sylancl 693 |
. . . 4
⊢ (𝜑 → (ran 𝑆 ∪ {𝑋}) ∈ V) |
53 | | fiuni 8217 |
. . . 4
⊢ ((ran
𝑆 ∪ {𝑋}) ∈ V → ∪ (ran 𝑆 ∪ {𝑋}) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
54 | 52, 53 | syl 17 |
. . 3
⊢ (𝜑 → ∪ (ran 𝑆 ∪ {𝑋}) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
55 | 28, 32, 54 | 3eqtr4d 2654 |
. 2
⊢ (𝜑 → 𝑋 = ∪ (ran 𝑆 ∪ {𝑋})) |
56 | 55, 23 | jca 553 |
1
⊢ (𝜑 → (𝑋 = ∪ (ran 𝑆 ∪ {𝑋}) ∧ (∏t‘𝐹) = (topGen‘(fi‘(ran
𝑆 ∪ {𝑋}))))) |