| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ptcmp.3 | . . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 2 |  | ptcmp.4 | . . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴⟶Comp) | 
| 3 | 2 | ffnd 6737 | . . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐴) | 
| 4 |  | eqid 2737 | . . . . . . . 8
⊢ {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} | 
| 5 | 4 | ptval 23578 | . . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹 Fn 𝐴) → (∏t‘𝐹) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) | 
| 6 | 1, 3, 5 | syl2anc 584 | . . . . . 6
⊢ (𝜑 →
(∏t‘𝐹) = (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))})) | 
| 7 |  | cmptop 23403 | . . . . . . . . . . 11
⊢ (𝑥 ∈ Comp → 𝑥 ∈ Top) | 
| 8 | 7 | ssriv 3987 | . . . . . . . . . 10
⊢ Comp
⊆ Top | 
| 9 |  | fss 6752 | . . . . . . . . . 10
⊢ ((𝐹:𝐴⟶Comp ∧ Comp ⊆ Top) →
𝐹:𝐴⟶Top) | 
| 10 | 2, 8, 9 | sylancl 586 | . . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶Top) | 
| 11 |  | ptcmp.2 | . . . . . . . . . 10
⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) | 
| 12 | 4, 11 | ptbasfi 23589 | . . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))) | 
| 13 | 1, 10, 12 | syl2anc 584 | . . . . . . . 8
⊢ (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))) | 
| 14 |  | uncom 4158 | . . . . . . . . . 10
⊢ (ran
𝑆 ∪ {𝑋}) = ({𝑋} ∪ ran 𝑆) | 
| 15 |  | ptcmp.1 | . . . . . . . . . . . 12
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) | 
| 16 | 15 | rneqi 5948 | . . . . . . . . . . 11
⊢ ran 𝑆 = ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) | 
| 17 | 16 | uneq2i 4165 | . . . . . . . . . 10
⊢ ({𝑋} ∪ ran 𝑆) = ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) | 
| 18 | 14, 17 | eqtri 2765 | . . . . . . . . 9
⊢ (ran
𝑆 ∪ {𝑋}) = ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) | 
| 19 | 18 | fveq2i 6909 | . . . . . . . 8
⊢
(fi‘(ran 𝑆
∪ {𝑋})) =
(fi‘({𝑋} ∪ ran
(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) | 
| 20 | 13, 19 | eqtr4di 2795 | . . . . . . 7
⊢ (𝜑 → {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))} = (fi‘(ran 𝑆 ∪ {𝑋}))) | 
| 21 | 20 | fveq2d 6910 | . . . . . 6
⊢ (𝜑 → (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) | 
| 22 | 6, 21 | eqtrd 2777 | . . . . 5
⊢ (𝜑 →
(∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) | 
| 23 | 22 | unieqd 4920 | . . . 4
⊢ (𝜑 → ∪ (∏t‘𝐹) = ∪
(topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) | 
| 24 |  | fibas 22984 | . . . . 5
⊢
(fi‘(ran 𝑆
∪ {𝑋})) ∈
TopBases | 
| 25 |  | unitg 22974 | . . . . 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 2793 | . . 3
⊢ (𝜑 → ∪ (∏t‘𝐹) = ∪
(fi‘(ran 𝑆 ∪
{𝑋}))) | 
| 28 |  | eqid 2737 | . . . . . 6
⊢
(∏t‘𝐹) = (∏t‘𝐹) | 
| 29 | 28 | ptuni 23602 | . . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = ∪
(∏t‘𝐹)) | 
| 30 | 1, 10, 29 | syl2anc 584 | . . . 4
⊢ (𝜑 → X𝑛 ∈
𝐴 ∪ (𝐹‘𝑛) = ∪
(∏t‘𝐹)) | 
| 31 | 11, 30 | eqtrid 2789 | . . 3
⊢ (𝜑 → 𝑋 = ∪
(∏t‘𝐹)) | 
| 32 |  | ptcmp.5 | . . . . . . 7
⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom
card)) | 
| 33 | 32 | pwexd 5379 | . . . . . 6
⊢ (𝜑 → 𝒫 𝑋 ∈ V) | 
| 34 |  | eqid 2737 | . . . . . . . . . . . 12
⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) | 
| 35 | 34 | mptpreima 6258 | . . . . . . . . . . 11
⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = {𝑤 ∈ 𝑋 ∣ (𝑤‘𝑘) ∈ 𝑢} | 
| 36 | 35 | ssrab3 4082 | . . . . . . . . . 10
⊢ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋 | 
| 37 | 32 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → 𝑋 ∈ (UFL ∩ dom
card)) | 
| 38 |  | elpw2g 5333 | . . . . . . . . . . 11
⊢ (𝑋 ∈ (UFL ∩ dom card)
→ ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋)) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ⊆ 𝑋)) | 
| 40 | 36, 39 | mpbiri 258 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋) | 
| 41 | 40 | ralrimivva 3202 | . . . . . . . 8
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋) | 
| 42 | 15 | fmpox 8092 | . . . . . . . 8
⊢
(∀𝑘 ∈
𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝒫 𝑋 ↔ 𝑆:∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝒫 𝑋) | 
| 43 | 41, 42 | sylib 218 | . . . . . . 7
⊢ (𝜑 → 𝑆:∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝒫 𝑋) | 
| 44 | 43 | frnd 6744 | . . . . . 6
⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝑋) | 
| 45 | 33, 44 | ssexd 5324 | . . . . 5
⊢ (𝜑 → ran 𝑆 ∈ V) | 
| 46 |  | snex 5436 | . . . . 5
⊢ {𝑋} ∈ V | 
| 47 |  | unexg 7763 | . . . . 5
⊢ ((ran
𝑆 ∈ V ∧ {𝑋} ∈ V) → (ran 𝑆 ∪ {𝑋}) ∈ V) | 
| 48 | 45, 46, 47 | sylancl 586 | . . . 4
⊢ (𝜑 → (ran 𝑆 ∪ {𝑋}) ∈ V) | 
| 49 |  | fiuni 9468 | . . . 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 511 | 1
⊢ (𝜑 → (𝑋 = ∪ (ran 𝑆 ∪ {𝑋}) ∧ (∏t‘𝐹) = (topGen‘(fi‘(ran
𝑆 ∪ {𝑋}))))) |