Step | Hyp | Ref
| Expression |
1 | | ptcmp.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | ptcmp.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶Comp) |
3 | 2 | ffnd 6546 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐴) |
4 | | eqid 2737 |
. . . . . . . 8
⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} |
5 | 4 | ptval 22467 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → (∏t‘𝐹) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
6 | 1, 3, 5 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 →
(∏t‘𝐹) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) |
7 | | cmptop 22292 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ Comp → 𝑥 ∈ Top) |
8 | 7 | ssriv 3905 |
. . . . . . . . . 10
⊢ Comp
⊆ Top |
9 | | fss 6562 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) →
𝐹:𝐴⟶Top) |
10 | 2, 8, 9 | sylancl 589 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶Top) |
11 | | ptcmp.2 |
. . . . . . . . . 10
⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) |
12 | 4, 11 | ptbasfi 22478 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))) |
13 | 1, 10, 12 | syl2anc 587 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))) |
14 | | uncom 4067 |
. . . . . . . . . 10
⊢ (ran
𝑆 ∪ {𝑋}) = ({𝑋} ∪ ran 𝑆) |
15 | | ptcmp.1 |
. . . . . . . . . . . 12
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) |
16 | 15 | rneqi 5806 |
. . . . . . . . . . 11
⊢ ran 𝑆 = ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) |
17 | 16 | uneq2i 4074 |
. . . . . . . . . 10
⊢ ({𝑋} ∪ ran 𝑆) = ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) |
18 | 14, 17 | eqtri 2765 |
. . . . . . . . 9
⊢ (ran
𝑆 ∪ {𝑋}) = ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) |
19 | 18 | fveq2i 6720 |
. . . . . . . 8
⊢
(fi‘(ran 𝑆
∪ {𝑋})) =
(fi‘({𝑋} ∪ ran
(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) |
20 | 13, 19 | eqtr4di 2796 |
. . . . . . 7
⊢ (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘(ran 𝑆 ∪ {𝑋}))) |
21 | 20 | fveq2d 6721 |
. . . . . 6
⊢ (𝜑 → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) |
22 | 6, 21 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 →
(∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) |
23 | 22 | unieqd 4833 |
. . . 4
⊢ (𝜑 → ∪ (∏t‘𝐹) = ∪
(topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) |
24 | | fibas 21874 |
. . . . 5
⊢
(fi‘(ran 𝑆
∪ {𝑋})) ∈
TopBases |
25 | | unitg 21864 |
. . . . 5
⊢
((fi‘(ran 𝑆
∪ {𝑋})) ∈ TopBases
→ ∪ (topGen‘(fi‘(ran 𝑆 ∪ {𝑋}))) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
26 | 24, 25 | ax-mp 5 |
. . . 4
⊢ ∪ (topGen‘(fi‘(ran 𝑆 ∪ {𝑋}))) = ∪
(fi‘(ran 𝑆 ∪
{𝑋})) |
27 | 23, 26 | eqtrdi 2794 |
. . 3
⊢ (𝜑 → ∪ (∏t‘𝐹) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
28 | | eqid 2737 |
. . . . . 6
⊢
(∏t‘𝐹) = (∏t‘𝐹) |
29 | 28 | ptuni 22491 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = ∪
(∏t‘𝐹)) |
30 | 1, 10, 29 | syl2anc 587 |
. . . 4
⊢ (𝜑 → X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = ∪
(∏t‘𝐹)) |
31 | 11, 30 | syl5eq 2790 |
. . 3
⊢ (𝜑 → 𝑋 = ∪
(∏t‘𝐹)) |
32 | | ptcmp.5 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom
card)) |
33 | 32 | pwexd 5272 |
. . . . . 6
⊢ (𝜑 → 𝒫 𝑋 ∈ V) |
34 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) |
35 | 34 | mptpreima 6101 |
. . . . . . . . . . 11
⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑢} |
36 | 35 | ssrab3 3995 |
. . . . . . . . . 10
⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋 |
37 | 32 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝑋 ∈ (UFL ∩ dom
card)) |
38 | | elpw2g 5237 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (UFL ∩ dom card)
→ ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋)) |
39 | 37, 38 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋)) |
40 | 36, 39 | mpbiri 261 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋) |
41 | 40 | ralrimivva 3112 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋) |
42 | 15 | fmpox 7837 |
. . . . . . . 8
⊢
(∀𝑘 ∈
𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ 𝑆:∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝒫 𝑋) |
43 | 41, 42 | sylib 221 |
. . . . . . 7
⊢ (𝜑 → 𝑆:∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝒫 𝑋) |
44 | 43 | frnd 6553 |
. . . . . 6
⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝑋) |
45 | 33, 44 | ssexd 5217 |
. . . . 5
⊢ (𝜑 → ran 𝑆 ∈ V) |
46 | | snex 5324 |
. . . . 5
⊢ {𝑋} ∈ V |
47 | | unexg 7534 |
. . . . 5
⊢ ((ran
𝑆 ∈ V ∧ {𝑋} ∈ V) → (ran 𝑆 ∪ {𝑋}) ∈ V) |
48 | 45, 46, 47 | sylancl 589 |
. . . 4
⊢ (𝜑 → (ran 𝑆 ∪ {𝑋}) ∈ V) |
49 | | fiuni 9044 |
. . . 4
⊢ ((ran
𝑆 ∪ {𝑋}) ∈ V → ∪ (ran 𝑆 ∪ {𝑋}) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
50 | 48, 49 | syl 17 |
. . 3
⊢ (𝜑 → ∪ (ran 𝑆 ∪ {𝑋}) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) |
51 | 27, 31, 50 | 3eqtr4d 2787 |
. 2
⊢ (𝜑 → 𝑋 = ∪ (ran 𝑆 ∪ {𝑋})) |
52 | 51, 22 | jca 515 |
1
⊢ (𝜑 → (𝑋 = ∪ (ran 𝑆 ∪ {𝑋}) ∧ (∏t‘𝐹) = (topGen‘(fi‘(ran
𝑆 ∪ {𝑋}))))) |