Step | Hyp | Ref
| Expression |
1 | | inss1 3833 |
. . 3
⊢ (UFL
∩ dom card) ⊆ UFL |
2 | | ptcmp.5 |
. . 3
⊢ (𝜑 → 𝑋 ∈ (UFL ∩ dom
card)) |
3 | 1, 2 | sseldi 3601 |
. 2
⊢ (𝜑 → 𝑋 ∈ UFL) |
4 | | ptcmp.1 |
. . . 4
⊢ 𝑆 = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) |
5 | | ptcmp.2 |
. . . 4
⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) |
6 | | ptcmp.3 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
7 | | ptcmp.4 |
. . . 4
⊢ (𝜑 → 𝐹:𝐴⟶Comp) |
8 | 4, 5, 6, 7, 2 | ptcmplem1 21856 |
. . 3
⊢ (𝜑 → (𝑋 = ∪ (ran 𝑆 ∪ {𝑋}) ∧ (∏t‘𝐹) = (topGen‘(fi‘(ran
𝑆 ∪ {𝑋}))))) |
9 | 8 | simpld 475 |
. 2
⊢ (𝜑 → 𝑋 = ∪ (ran 𝑆 ∪ {𝑋})) |
10 | 8 | simprd 479 |
. 2
⊢ (𝜑 →
(∏t‘𝐹) = (topGen‘(fi‘(ran 𝑆 ∪ {𝑋})))) |
11 | | elpwi 4168 |
. . . . . 6
⊢ (𝑦 ∈ 𝒫 ran 𝑆 → 𝑦 ⊆ ran 𝑆) |
12 | 6 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝐴 ∈ 𝑉) |
13 | 7 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝐹:𝐴⟶Comp) |
14 | 2 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝑋 ∈ (UFL ∩ dom
card)) |
15 | | simplrl 800 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝑦 ⊆ ran 𝑆) |
16 | | simplrr 801 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → 𝑋 = ∪ 𝑦) |
17 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) → ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
18 | | imaeq2 5462 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑢 → (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑧) = (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) |
19 | 18 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑢 → ((◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑧) ∈ 𝑦 ↔ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑦)) |
20 | 19 | cbvrabv 3199 |
. . . . . . . . 9
⊢ {𝑧 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑧) ∈ 𝑦} = {𝑢 ∈ (𝐹‘𝑘) ∣ (◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝑦} |
21 | 4, 5, 12, 13, 14, 15, 16, 17, 20 | ptcmplem4 21859 |
. . . . . . . 8
⊢ ¬
((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
22 | | iman 440 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) ↔ ¬ ((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) ∧ ¬ ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
23 | 21, 22 | mpbir 221 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ⊆ ran 𝑆 ∧ 𝑋 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
24 | 23 | expr 643 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ⊆ ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
25 | 11, 24 | sylan2 491 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝒫 ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
26 | 25 | adantlr 751 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑦 ∈ 𝒫 ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
27 | | selpw 4165 |
. . . . . . 7
⊢ (𝑦 ∈ 𝒫 (ran 𝑆 ∪ {𝑋}) ↔ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) |
28 | | eldif 3584 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝒫 (ran 𝑆 ∪ {𝑋}) ∖ 𝒫 ran 𝑆) ↔ (𝑦 ∈ 𝒫 (ran 𝑆 ∪ {𝑋}) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆)) |
29 | | elpwunsn 4224 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝒫 (ran 𝑆 ∪ {𝑋}) ∖ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦) |
30 | 28, 29 | sylbir 225 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝒫 (ran 𝑆 ∪ {𝑋}) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦) |
31 | 27, 30 | sylanbr 490 |
. . . . . 6
⊢ ((𝑦 ⊆ (ran 𝑆 ∪ {𝑋}) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦) |
32 | 31 | adantll 750 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → 𝑋 ∈ 𝑦) |
33 | | snssi 4339 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑦 → {𝑋} ⊆ 𝑦) |
34 | 33 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → {𝑋} ⊆ 𝑦) |
35 | | snfi 8038 |
. . . . . . . . 9
⊢ {𝑋} ∈ Fin |
36 | 35 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → {𝑋} ∈ Fin) |
37 | | elfpw 8268 |
. . . . . . . 8
⊢ ({𝑋} ∈ (𝒫 𝑦 ∩ Fin) ↔ ({𝑋} ⊆ 𝑦 ∧ {𝑋} ∈ Fin)) |
38 | 34, 36, 37 | sylanbrc 698 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → {𝑋} ∈ (𝒫 𝑦 ∩ Fin)) |
39 | | unisng 4452 |
. . . . . . . . 9
⊢ (𝑋 ∈ 𝑦 → ∪ {𝑋} = 𝑋) |
40 | 39 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝑋 ∈ 𝑦 → 𝑋 = ∪ {𝑋}) |
41 | 40 | adantl 482 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → 𝑋 = ∪ {𝑋}) |
42 | | unieq 4444 |
. . . . . . . . 9
⊢ (𝑧 = {𝑋} → ∪ 𝑧 = ∪
{𝑋}) |
43 | 42 | eqeq2d 2632 |
. . . . . . . 8
⊢ (𝑧 = {𝑋} → (𝑋 = ∪ 𝑧 ↔ 𝑋 = ∪ {𝑋})) |
44 | 43 | rspcev 3309 |
. . . . . . 7
⊢ (({𝑋} ∈ (𝒫 𝑦 ∩ Fin) ∧ 𝑋 = ∪
{𝑋}) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
45 | 38, 41, 44 | syl2anc 693 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
46 | 45 | a1d 25 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ 𝑋 ∈ 𝑦) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
47 | 32, 46 | syldan 487 |
. . . 4
⊢ (((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) ∧ ¬ 𝑦 ∈ 𝒫 ran 𝑆) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
48 | 26, 47 | pm2.61dan 832 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ⊆ (ran 𝑆 ∪ {𝑋})) → (𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧)) |
49 | 48 | impr 649 |
. 2
⊢ ((𝜑 ∧ (𝑦 ⊆ (ran 𝑆 ∪ {𝑋}) ∧ 𝑋 = ∪ 𝑦)) → ∃𝑧 ∈ (𝒫 𝑦 ∩ Fin)𝑋 = ∪ 𝑧) |
50 | 3, 9, 10, 49 | alexsub 21849 |
1
⊢ (𝜑 →
(∏t‘𝐹) ∈ Comp) |