| Step | Hyp | Ref
| Expression |
| 1 | | ptcmp.5 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom
card)) |
| 2 | 1 | elin1d 4204 |
. 2
⊢ (𝜑 → 𝑋 ∈ UFL) |
| 3 | | ptcmp.1 |
. . . 4
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) |
| 4 | | ptcmp.2 |
. . . 4
⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) |
| 5 | | ptcmp.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 6 | | ptcmp.4 |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶Comp) |
| 7 | 3, 4, 5, 6, 1 | ptcmplem1 24060 |
. . 3
⊢ (𝜑 → (𝑋 = ∪ (ran 𝑆 ∪ {𝑋}) ∧ (∏t‘𝐹) = (topGen‘(fi‘(ran
𝑆 ∪ {𝑋}))))) |
| 8 | 7 | simpld 494 |
. 2
⊢ (𝜑 → 𝑋 = ∪ (ran 𝑆 ∪ {𝑋})) |
| 9 | 7 | simprd 495 |
. 2
⊢ (𝜑 →
(∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) |
| 10 | | elpwi 4607 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 ran 𝑆 → 𝑦 ⊆ ran 𝑆) |
| 11 | 5 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝐴 ∈ 𝑉) |
| 12 | 6 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝐹:𝐴⟶Comp) |
| 13 | 1 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝑋 ∈ (UFL ∩ dom
card)) |
| 14 | | simplrl 777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝑦 ⊆ ran 𝑆) |
| 15 | | simplrr 778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝑋 = ∪ 𝑦) |
| 16 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
| 17 | | imaeq2 6074 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑢 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑧) = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) |
| 18 | 17 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑢 → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑧) ∈ 𝑦 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑦)) |
| 19 | 18 | cbvrabv 3447 |
. . . . . . . . 9
⊢ {𝑧 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑧) ∈ 𝑦} = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑦} |
| 20 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | ptcmplem4 24063 |
. . . . . . . 8
⊢ ¬
((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
| 21 | | iman 401 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) ↔ ¬ ((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
| 22 | 20, 21 | mpbir 231 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
| 23 | 22 | expr 456 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ⊆ ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
| 24 | 10, 23 | sylan2 593 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
| 25 | 24 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑦 ∈ 𝒫 ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
| 26 | | velpw 4605 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 (ran 𝑆 ∪ {𝑋}) ↔ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) |
| 27 | | eldif 3961 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝒫 (ran 𝑆 ∪ {𝑋}) ∖ 𝒫 ran 𝑆) ↔ (𝑦 ∈ 𝒫 (ran 𝑆 ∪ {𝑋}) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆)) |
| 28 | | elpwunsn 4684 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝒫 (ran 𝑆 ∪ {𝑋}) ∖ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦) |
| 29 | 27, 28 | sylbir 235 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝒫 (ran 𝑆 ∪ {𝑋}) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦) |
| 30 | 26, 29 | sylanbr 582 |
. . . . . 6
⊢ ((𝑦 ⊆ (ran 𝑆 ∪ {𝑋}) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦) |
| 31 | 30 | adantll 714 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦) |
| 32 | | snssi 4808 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑦 → {𝑋} ⊆ 𝑦) |
| 33 | 32 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → {𝑋} ⊆ 𝑦) |
| 34 | | snfi 9083 |
. . . . . . . 8
⊢ {𝑋} ∈ Fin |
| 35 | | elfpw 9394 |
. . . . . . . 8
⊢ ({𝑋} ∈ (𝒫 𝑦 ∩ Fin) ↔ ({𝑋} ⊆ 𝑦 ∧ {𝑋} ∈ Fin)) |
| 36 | 33, 34, 35 | sylanblrc 590 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → {𝑋} ∈ (𝒫 𝑦 ∩ Fin)) |
| 37 | | unisng 4925 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑦 → ∪ {𝑋} = 𝑋) |
| 38 | 37 | eqcomd 2743 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑦 → 𝑋 = ∪ {𝑋}) |
| 39 | 38 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → 𝑋 = ∪ {𝑋}) |
| 40 | | unieq 4918 |
. . . . . . . 8
⊢ (𝑧 = {𝑋} → ∪ 𝑧 = ∪
{𝑋}) |
| 41 | 40 | rspceeqv 3645 |
. . . . . . 7
⊢ (({𝑋} ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑋 = ∪
{𝑋}) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
| 42 | 36, 39, 41 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
| 43 | 42 | a1d 25 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
| 44 | 31, 43 | syldan 591 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
| 45 | 25, 44 | pm2.61dan 813 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
| 46 | 45 | impr 454 |
. 2
⊢ ((𝜑 ∧ (𝑦 ⊆ (ran 𝑆 ∪ {𝑋}) ∧ 𝑋 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
| 47 | 2, 8, 9, 46 | alexsub 24053 |
1
⊢ (𝜑 →
(∏t‘𝐹) ∈ Comp) |