Step | Hyp | Ref
| Expression |
1 | | ptcmp.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | ptcmp.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶Comp) |
3 | 2 | ffnd 6257 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐴) |
4 | | eqid 2799 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} |
5 | 4 | ptval 21702 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → (∏t‘𝐹) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
6 | 1, 3, 5 | syl2anc 580 |
. . . . . 6
⊢ (𝜑 →
(∏t‘𝐹) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
7 | | cmptop 21527 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ Comp → 𝑥 ∈ Top) |
8 | 7 | ssriv 3802 |
. . . . . . . . . 10
⊢ Comp
⊆ Top |
9 | | fss 6269 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) →
𝐹:𝐴⟶Top) |
10 | 2, 8, 9 | sylancl 581 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶Top) |
11 | | ptcmp.2 |
. . . . . . . . . 10
⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) |
12 | 4, 11 | ptbasfi 21713 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))) |
13 | 1, 10, 12 | syl2anc 580 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))) |
14 | | uncom 3955 |
. . . . . . . . . 10
⊢ (ran
𝑆 ∪ {𝑋}) = ({𝑋} ∪ ran 𝑆) |
15 | | ptcmp.1 |
. . . . . . . . . . . 12
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) |
16 | 15 | rneqi 5555 |
. . . . . . . . . . 11
⊢ ran 𝑆 = ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) |
17 | 16 | uneq2i 3962 |
. . . . . . . . . 10
⊢ ({𝑋} ∪ ran 𝑆) = ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) |
18 | 14, 17 | eqtri 2821 |
. . . . . . . . 9
⊢ (ran
𝑆 ∪ {𝑋}) = ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) |
19 | 18 | fveq2i 6414 |
. . . . . . . 8
⊢
(fi‘(ran 𝑆
∪ {𝑋})) =
(fi‘({𝑋} ∪ ran
(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) |
20 | 13, 19 | syl6eqr 2851 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘(ran 𝑆 ∪ {𝑋}))) |
21 | 20 | fveq2d 6415 |
. . . . . 6
⊢ (𝜑 → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) |
22 | 6, 21 | eqtrd 2833 |
. . . . 5
⊢ (𝜑 →
(∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) |
23 | 22 | unieqd 4638 |
. . . 4
⊢ (𝜑 → ∪ (∏t‘𝐹) = ∪
(topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) |
24 | | fibas 21110 |
. . . . 5
⊢
(fi‘(ran 𝑆
∪ {𝑋})) ∈
TopBases |
25 | | unitg 21100 |
. . . . 5
⊢
((fi‘(ran 𝑆
∪ {𝑋})) ∈ TopBases
→ ∪ (topGen‘(fi‘(ran 𝑆 ∪ {𝑋}))) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
26 | 24, 25 | ax-mp 5 |
. . . 4
⊢ ∪ (topGen‘(fi‘(ran 𝑆 ∪ {𝑋}))) = ∪
(fi‘(ran 𝑆 ∪
{𝑋})) |
27 | 23, 26 | syl6eq 2849 |
. . 3
⊢ (𝜑 → ∪ (∏t‘𝐹) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
28 | | eqid 2799 |
. . . . . 6
⊢
(∏t‘𝐹) = (∏t‘𝐹) |
29 | 28 | ptuni 21726 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = ∪
(∏t‘𝐹)) |
30 | 1, 10, 29 | syl2anc 580 |
. . . 4
⊢ (𝜑 → X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = ∪
(∏t‘𝐹)) |
31 | 11, 30 | syl5eq 2845 |
. . 3
⊢ (𝜑 → 𝑋 = ∪
(∏t‘𝐹)) |
32 | | ptcmp.5 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom
card)) |
33 | 32 | pwexd 5049 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝑋 ∈ V) |
34 | | eqid 2799 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) |
35 | 34 | mptpreima 5847 |
. . . . . . . . . . 11
⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑢} |
36 | | ssrab2 3883 |
. . . . . . . . . . 11
⊢ {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑢} ⊆ 𝑋 |
37 | 35, 36 | eqsstri 3831 |
. . . . . . . . . 10
⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋 |
38 | 32 | adantr 473 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝑋 ∈ (UFL ∩ dom
card)) |
39 | | elpw2g 5019 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (UFL ∩ dom card)
→ ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋)) |
40 | 38, 39 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋)) |
41 | 37, 40 | mpbiri 250 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋) |
42 | 41 | ralrimivva 3152 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋) |
43 | 15 | fmpt2x 7472 |
. . . . . . . 8
⊢
(∀𝑘 ∈
𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ 𝑆:∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝒫 𝑋) |
44 | 42, 43 | sylib 210 |
. . . . . . 7
⊢ (𝜑 → 𝑆:∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝒫 𝑋) |
45 | 44 | frnd 6263 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝑋) |
46 | 33, 45 | ssexd 5000 |
. . . . 5
⊢ (𝜑 → ran 𝑆 ∈ V) |
47 | | snex 5099 |
. . . . 5
⊢ {𝑋} ∈ V |
48 | | unexg 7193 |
. . . . 5
⊢ ((ran
𝑆 ∈ V ∧ {𝑋} ∈ V) → (ran 𝑆 ∪ {𝑋}) ∈ V) |
49 | 46, 47, 48 | sylancl 581 |
. . . 4
⊢ (𝜑 → (ran 𝑆 ∪ {𝑋}) ∈ V) |
50 | | fiuni 8576 |
. . . 4
⊢ ((ran
𝑆 ∪ {𝑋}) ∈ V → ∪ (ran 𝑆 ∪ {𝑋}) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
51 | 49, 50 | syl 17 |
. . 3
⊢ (𝜑 → ∪ (ran 𝑆 ∪ {𝑋}) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
52 | 27, 31, 51 | 3eqtr4d 2843 |
. 2
⊢ (𝜑 → 𝑋 = ∪ (ran 𝑆 ∪ {𝑋})) |
53 | 52, 22 | jca 508 |
1
⊢ (𝜑 → (𝑋 = ∪ (ran 𝑆 ∪ {𝑋}) ∧ (∏t‘𝐹) = (topGen‘(fi‘(ran
𝑆 ∪ {𝑋}))))) |