| Step | Hyp | Ref
| Expression |
| 1 | | eldif 3961 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ↔ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) |
| 2 | | alexsub.3 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐽 = (topGen‘(fi‘𝐵))) |
| 3 | 2 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↔ 𝑦 ∈ (topGen‘(fi‘𝐵)))) |
| 4 | 3 | anbi1d 631 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦) ↔ (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦))) |
| 5 | 4 | biimpa 476 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦)) |
| 6 | 5 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → (𝑦 ∈ (topGen‘(fi‘𝐵)) ∧ 𝑥 ∈ 𝑦)) |
| 7 | | tg2 22972 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈
(topGen‘(fi‘𝐵))
∧ 𝑥 ∈ 𝑦) → ∃𝑧 ∈ (fi‘𝐵)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) |
| 8 | 6, 7 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → ∃𝑧 ∈ (fi‘𝐵)(𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦)) |
| 9 | | alexsub.5 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ (UFil‘𝑋)) |
| 10 | | ufilfil 23912 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) |
| 11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹 ∈ (Fil‘𝑋)) |
| 12 | 11 | ad3antrrr 730 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝐹 ∈ (Fil‘𝑋)) |
| 13 | | alexsub.2 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑋 = ∪ 𝐵) |
| 14 | 9 | elfvexd 6945 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑋 ∈ V) |
| 15 | 13, 14 | eqeltrrd 2842 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∪ 𝐵
∈ V) |
| 16 | | uniexb 7784 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐵 ∈ V ↔ ∪ 𝐵
∈ V) |
| 17 | 15, 16 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐵 ∈ V) |
| 18 | | elfi2 9454 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐵 ∈ V → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖
{∅})𝑧 = ∩ 𝑦)) |
| 19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = ∩
𝑦)) |
| 20 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → (𝑧 ∈ (fi‘𝐵) ↔ ∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = ∩
𝑦)) |
| 21 | 11 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦))
→ 𝐹 ∈
(Fil‘𝑋)) |
| 22 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)
∧ 𝑧 ∈ 𝑦)) → ¬ 𝑥 ∈ ∪ (𝐵
∖ 𝐹)) |
| 23 | | intss1 4963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑧 ∈ 𝑦 → ∩ 𝑦 ⊆ 𝑧) |
| 24 | 23 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝑥 ∈ ∩ 𝑦)
∧ 𝑧 ∈ 𝑦) → ∩ 𝑦
⊆ 𝑧) |
| 25 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝑥 ∈ ∩ 𝑦)
∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ ∩ 𝑦) |
| 26 | 24, 25 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
∧ 𝑥 ∈ ∩ 𝑦)
∧ 𝑧 ∈ 𝑦) → 𝑥 ∈ 𝑧) |
| 27 | 26 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)
∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑥 ∈ 𝑧) |
| 28 | | eldifsn 4786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
↔ (𝑦 ∈ (𝒫
𝐵 ∩ Fin) ∧ 𝑦 ≠ ∅)) |
| 29 | 28 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
→ 𝑦 ∈ (𝒫
𝐵 ∩
Fin)) |
| 30 | 29 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦))
→ 𝑦 ∈ (𝒫
𝐵 ∩
Fin)) |
| 31 | | elfpw 9394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) ↔ (𝑦 ⊆ 𝐵 ∧ 𝑦 ∈ Fin)) |
| 32 | 31 | simplbi 497 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ⊆ 𝐵) |
| 33 | 30, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦))
→ 𝑦 ⊆ 𝐵) |
| 34 | 33 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦))
∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐵) |
| 35 | 34 | anasss 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)
∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝐵) |
| 36 | 35 | anim1i 615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)
∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹)) |
| 37 | | eldif 3961 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑧 ∈ (𝐵 ∖ 𝐹) ↔ (𝑧 ∈ 𝐵 ∧ ¬ 𝑧 ∈ 𝐹)) |
| 38 | 36, 37 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)
∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑧 ∈ (𝐵 ∖ 𝐹)) |
| 39 | | elunii 4912 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑥 ∈ 𝑧 ∧ 𝑧 ∈ (𝐵 ∖ 𝐹)) → 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)) |
| 40 | 27, 38, 39 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)
∧ 𝑧 ∈ 𝑦)) ∧ ¬ 𝑧 ∈ 𝐹) → 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)) |
| 41 | 40 | ex 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)
∧ 𝑧 ∈ 𝑦)) → (¬ 𝑧 ∈ 𝐹 → 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) |
| 42 | 22, 41 | mt3d 148 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ ((𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦)
∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝐹) |
| 43 | 42 | expr 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦))
→ (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝐹)) |
| 44 | 43 | ssrdv 3989 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦))
→ 𝑦 ⊆ 𝐹) |
| 45 | | eldifsni 4790 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})
→ 𝑦 ≠
∅) |
| 46 | 45 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦))
→ 𝑦 ≠
∅) |
| 47 | | elinel2 4202 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑦 ∈ (𝒫 𝐵 ∩ Fin) → 𝑦 ∈ Fin) |
| 48 | 30, 47 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦))
→ 𝑦 ∈
Fin) |
| 49 | | elfir 9455 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ⊆ 𝐹 ∧ 𝑦 ≠ ∅ ∧ 𝑦 ∈ Fin)) → ∩ 𝑦
∈ (fi‘𝐹)) |
| 50 | 21, 44, 46, 48, 49 | syl13anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦))
→ ∩ 𝑦 ∈ (fi‘𝐹)) |
| 51 | | filfi 23867 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐹 ∈ (Fil‘𝑋) → (fi‘𝐹) = 𝐹) |
| 52 | 21, 51 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦))
→ (fi‘𝐹) = 𝐹) |
| 53 | 50, 52 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅}) ∧ 𝑥 ∈ ∩ 𝑦))
→ ∩ 𝑦 ∈ 𝐹) |
| 54 | 53 | expr 456 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) →
(𝑥 ∈ ∩ 𝑦
→ ∩ 𝑦 ∈ 𝐹)) |
| 55 | | eleq2 2830 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = ∩
𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ∩ 𝑦)) |
| 56 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 = ∩
𝑦 → (𝑧 ∈ 𝐹 ↔ ∩ 𝑦 ∈ 𝐹)) |
| 57 | 55, 56 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 = ∩
𝑦 → ((𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹) ↔ (𝑥 ∈ ∩ 𝑦 → ∩ 𝑦
∈ 𝐹))) |
| 58 | 54, 57 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})) →
(𝑧 = ∩ 𝑦
→ (𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹))) |
| 59 | 58 | rexlimdva 3155 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → (∃𝑦 ∈ ((𝒫 𝐵 ∩ Fin) ∖ {∅})𝑧 = ∩
𝑦 → (𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹))) |
| 60 | 20, 59 | sylbid 240 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → (𝑧 ∈ (fi‘𝐵) → (𝑥 ∈ 𝑧 → 𝑧 ∈ 𝐹))) |
| 61 | 60 | imp32 418 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ 𝑥 ∈ 𝑧)) → 𝑧 ∈ 𝐹) |
| 62 | 61 | adantrrr 725 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ 𝐹) |
| 63 | 62 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ∈ 𝐹) |
| 64 | | elssuni 4937 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ 𝐽 → 𝑦 ⊆ ∪ 𝐽) |
| 65 | 64 | ad2antrl 728 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ⊆ ∪ 𝐽) |
| 66 | | fibas 22984 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(fi‘𝐵) ∈
TopBases |
| 67 | | tgtopon 22978 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((fi‘𝐵) ∈
TopBases → (topGen‘(fi‘𝐵)) ∈ (TopOn‘∪ (fi‘𝐵))) |
| 68 | 66, 67 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(topGen‘(fi‘𝐵)) ∈ (TopOn‘∪ (fi‘𝐵)) |
| 69 | 2, 68 | eqeltrdi 2849 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ (fi‘𝐵))) |
| 70 | | fiuni 9468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐵 ∈ V → ∪ 𝐵 =
∪ (fi‘𝐵)) |
| 71 | 17, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ∪ 𝐵 =
∪ (fi‘𝐵)) |
| 72 | 13, 71 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑋 = ∪
(fi‘𝐵)) |
| 73 | 72 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (TopOn‘𝑋) = (TopOn‘∪ (fi‘𝐵))) |
| 74 | 69, 73 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
| 75 | | toponuni 22920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
| 76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
| 77 | 76 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑋 = ∪ 𝐽) |
| 78 | 65, 77 | sseqtrrd 4021 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ⊆ 𝑋) |
| 79 | 78 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ⊆ 𝑋) |
| 80 | | simprrr 782 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑧 ⊆ 𝑦) |
| 81 | | filss 23861 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑧 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑋 ∧ 𝑧 ⊆ 𝑦)) → 𝑦 ∈ 𝐹) |
| 82 | 12, 63, 79, 80, 81 | syl13anc 1374 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) ∧ (𝑧 ∈ (fi‘𝐵) ∧ (𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑦))) → 𝑦 ∈ 𝐹) |
| 83 | 8, 82 | rexlimddv 3161 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ (𝑦 ∈ 𝐽 ∧ 𝑥 ∈ 𝑦)) → 𝑦 ∈ 𝐹) |
| 84 | 83 | expr 456 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) ∧ 𝑦 ∈ 𝐽) → (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹)) |
| 85 | 84 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹))) → ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹)) |
| 86 | 85 | expr 456 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹) → ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹))) |
| 87 | 86 | imdistanda 571 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑥 ∈ 𝑋 ∧ ¬ 𝑥 ∈ ∪ (𝐵 ∖ 𝐹)) → (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹)))) |
| 88 | 1, 87 | biimtrid 242 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) → (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹)))) |
| 89 | | flimopn 23983 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋)) → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹)))) |
| 90 | 74, 11, 89 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (𝐽 fLim 𝐹) ↔ (𝑥 ∈ 𝑋 ∧ ∀𝑦 ∈ 𝐽 (𝑥 ∈ 𝑦 → 𝑦 ∈ 𝐹)))) |
| 91 | 88, 90 | sylibrd 259 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) → 𝑥 ∈ (𝐽 fLim 𝐹))) |
| 92 | 91 | ssrdv 3989 |
. . . . . . 7
⊢ (𝜑 → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) ⊆ (𝐽 fLim 𝐹)) |
| 93 | | alexsub.6 |
. . . . . . 7
⊢ (𝜑 → (𝐽 fLim 𝐹) = ∅) |
| 94 | | sseq0 4403 |
. . . . . . 7
⊢ (((𝑋 ∖ ∪ (𝐵
∖ 𝐹)) ⊆ (𝐽 fLim 𝐹) ∧ (𝐽 fLim 𝐹) = ∅) → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅) |
| 95 | 92, 93, 94 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑋 ∖ ∪ (𝐵 ∖ 𝐹)) = ∅) |
| 96 | | ssdif0 4366 |
. . . . . 6
⊢ (𝑋 ⊆ ∪ (𝐵
∖ 𝐹) ↔ (𝑋 ∖ ∪ (𝐵
∖ 𝐹)) =
∅) |
| 97 | 95, 96 | sylibr 234 |
. . . . 5
⊢ (𝜑 → 𝑋 ⊆ ∪ (𝐵 ∖ 𝐹)) |
| 98 | | difss 4136 |
. . . . . . 7
⊢ (𝐵 ∖ 𝐹) ⊆ 𝐵 |
| 99 | 98 | unissi 4916 |
. . . . . 6
⊢ ∪ (𝐵
∖ 𝐹) ⊆ ∪ 𝐵 |
| 100 | 99, 13 | sseqtrrid 4027 |
. . . . 5
⊢ (𝜑 → ∪ (𝐵
∖ 𝐹) ⊆ 𝑋) |
| 101 | 97, 100 | eqssd 4001 |
. . . 4
⊢ (𝜑 → 𝑋 = ∪ (𝐵 ∖ 𝐹)) |
| 102 | 101, 98 | jctil 519 |
. . 3
⊢ (𝜑 → ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) |
| 103 | 17 | difexd 5331 |
. . . . 5
⊢ (𝜑 → (𝐵 ∖ 𝐹) ∈ V) |
| 104 | 103 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → (𝐵 ∖ 𝐹) ∈ V) |
| 105 | | sseq1 4009 |
. . . . . . . 8
⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝑥 ⊆ 𝐵 ↔ (𝐵 ∖ 𝐹) ⊆ 𝐵)) |
| 106 | | unieq 4918 |
. . . . . . . . 9
⊢ (𝑥 = (𝐵 ∖ 𝐹) → ∪ 𝑥 = ∪
(𝐵 ∖ 𝐹)) |
| 107 | 106 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝑋 = ∪ 𝑥 ↔ 𝑋 = ∪ (𝐵 ∖ 𝐹))) |
| 108 | 105, 107 | anbi12d 632 |
. . . . . . 7
⊢ (𝑥 = (𝐵 ∖ 𝐹) → ((𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥) ↔ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹)))) |
| 109 | 108 | anbi2d 630 |
. . . . . 6
⊢ (𝑥 = (𝐵 ∖ 𝐹) → ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) ↔ (𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))))) |
| 110 | | pweq 4614 |
. . . . . . . 8
⊢ (𝑥 = (𝐵 ∖ 𝐹) → 𝒫 𝑥 = 𝒫 (𝐵 ∖ 𝐹)) |
| 111 | 110 | ineq1d 4219 |
. . . . . . 7
⊢ (𝑥 = (𝐵 ∖ 𝐹) → (𝒫 𝑥 ∩ Fin) = (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) |
| 112 | 111 | rexeqdv 3327 |
. . . . . 6
⊢ (𝑥 = (𝐵 ∖ 𝐹) → (∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦 ↔ ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)) |
| 113 | 109, 112 | imbi12d 344 |
. . . . 5
⊢ (𝑥 = (𝐵 ∖ 𝐹) → (((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) ↔ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦))) |
| 114 | | alexsub.4 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐵 ∧ 𝑋 = ∪ 𝑥)) → ∃𝑦 ∈ (𝒫 𝑥 ∩ Fin)𝑋 = ∪ 𝑦) |
| 115 | 113, 114 | vtoclg 3554 |
. . . 4
⊢ ((𝐵 ∖ 𝐹) ∈ V → ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦)) |
| 116 | 104, 115 | mpcom 38 |
. . 3
⊢ ((𝜑 ∧ ((𝐵 ∖ 𝐹) ⊆ 𝐵 ∧ 𝑋 = ∪ (𝐵 ∖ 𝐹))) → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦) |
| 117 | 102, 116 | mpdan 687 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦) |
| 118 | | unieq 4918 |
. . . . . . 7
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∪ ∅) |
| 119 | | uni0 4935 |
. . . . . . 7
⊢ ∪ ∅ = ∅ |
| 120 | 118, 119 | eqtrdi 2793 |
. . . . . 6
⊢ (𝑦 = ∅ → ∪ 𝑦 =
∅) |
| 121 | 120 | neeq2d 3001 |
. . . . 5
⊢ (𝑦 = ∅ → (𝑋 ≠ ∪ 𝑦
↔ 𝑋 ≠
∅)) |
| 122 | | difssd 4137 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → (𝑋 ∖ 𝑧) ⊆ 𝑋) |
| 123 | 122 | ralrimivw 3150 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → ∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ⊆ 𝑋) |
| 124 | | riinn0 5083 |
. . . . . . . . . 10
⊢
((∀𝑧 ∈
𝑦 (𝑋 ∖ 𝑧) ⊆ 𝑋 ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩
𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩
𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) |
| 125 | 123, 124 | sylan 580 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩
𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩
𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) |
| 126 | 14 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ∈ V) |
| 127 | 126 | difexd 5331 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∖ 𝑧) ∈ V) |
| 128 | 127 | ralrimivw 3150 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∀𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) ∈ V) |
| 129 | | dfiin2g 5032 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
𝑦 (𝑋 ∖ 𝑧) ∈ V → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)}) |
| 130 | 128, 129 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)}) |
| 131 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) |
| 132 | 131 | rnmpt 5968 |
. . . . . . . . . . 11
⊢ ran
(𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)} |
| 133 | 132 | inteqi 4950 |
. . . . . . . . . 10
⊢ ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∩ {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)} |
| 134 | 130, 133 | eqtr4di 2795 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧))) |
| 135 | 125, 134 | eqtrd 2777 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩
𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧))) |
| 136 | 11 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝐹 ∈ (Fil‘𝑋)) |
| 137 | | elfpw 9394 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) ↔ (𝑦 ⊆ (𝐵 ∖ 𝐹) ∧ 𝑦 ∈ Fin)) |
| 138 | 137 | simplbi 497 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) → 𝑦 ⊆ (𝐵 ∖ 𝐹)) |
| 139 | 138 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ (𝐵 ∖ 𝐹)) |
| 140 | 139 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ (𝐵 ∖ 𝐹)) |
| 141 | 140 | eldifbd 3964 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → ¬ 𝑧 ∈ 𝐹) |
| 142 | 9 | ad3antrrr 730 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝐹 ∈ (UFil‘𝑋)) |
| 143 | 139 | difss2d 4139 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ⊆ 𝐵) |
| 144 | 143 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ 𝐵) |
| 145 | | elssuni 4937 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ 𝐵 → 𝑧 ⊆ ∪ 𝐵) |
| 146 | 144, 145 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ ∪ 𝐵) |
| 147 | 13 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑋 = ∪ 𝐵) |
| 148 | 146, 147 | sseqtrrd 4021 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → 𝑧 ⊆ 𝑋) |
| 149 | | ufilb 23914 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑧 ⊆ 𝑋) → (¬ 𝑧 ∈ 𝐹 ↔ (𝑋 ∖ 𝑧) ∈ 𝐹)) |
| 150 | 142, 148,
149 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (¬ 𝑧 ∈ 𝐹 ↔ (𝑋 ∖ 𝑧) ∈ 𝐹)) |
| 151 | 141, 150 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (𝑋 ∖ 𝑧) ∈ 𝐹) |
| 152 | 151 | fmpttd 7135 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)):𝑦⟶𝐹) |
| 153 | 152 | frnd 6744 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ⊆ 𝐹) |
| 154 | 131, 151 | dmmptd 6713 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = 𝑦) |
| 155 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ≠ ∅) |
| 156 | 154, 155 | eqnetrd 3008 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → dom (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅) |
| 157 | | dm0rn0 5935 |
. . . . . . . . . . 11
⊢ (dom
(𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∅ ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) = ∅) |
| 158 | 157 | necon3bii 2993 |
. . . . . . . . . 10
⊢ (dom
(𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅ ↔ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅) |
| 159 | 156, 158 | sylib 218 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅) |
| 160 | | elinel2 4202 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin) → 𝑦 ∈ Fin) |
| 161 | 160 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑦 ∈ Fin) |
| 162 | | abrexfi 9392 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ Fin → {𝑥 ∣ ∃𝑧 ∈ 𝑦 𝑥 = (𝑋 ∖ 𝑧)} ∈ Fin) |
| 163 | 132, 162 | eqeltrid 2845 |
. . . . . . . . . 10
⊢ (𝑦 ∈ Fin → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin) |
| 164 | 161, 163 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin) |
| 165 | | filintn0 23869 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ⊆ 𝐹 ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅ ∧ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ∈ Fin)) → ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅) |
| 166 | 136, 153,
159, 164, 165 | syl13anc 1374 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∩ ran (𝑧 ∈ 𝑦 ↦ (𝑋 ∖ 𝑧)) ≠ ∅) |
| 167 | 135, 166 | eqnetrd 3008 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∩ ∩
𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) ≠ ∅) |
| 168 | | disj3 4454 |
. . . . . . . 8
⊢ ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∅ ↔ 𝑋 = (𝑋 ∖ ∩
𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))) |
| 169 | 168 | necon3bii 2993 |
. . . . . . 7
⊢ ((𝑋 ∩ ∩ 𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) ≠ ∅ ↔ 𝑋 ≠ (𝑋 ∖ ∩
𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))) |
| 170 | 167, 169 | sylib 218 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ (𝑋 ∖ ∩
𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧))) |
| 171 | | iundif2 5074 |
. . . . . . 7
⊢ ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = (𝑋 ∖ ∩
𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) |
| 172 | | dfss4 4269 |
. . . . . . . . . 10
⊢ (𝑧 ⊆ 𝑋 ↔ (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧) |
| 173 | 148, 172 | sylib 218 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) ∧ 𝑧 ∈ 𝑦) → (𝑋 ∖ (𝑋 ∖ 𝑧)) = 𝑧) |
| 174 | 173 | iuneq2dv 5016 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = ∪
𝑧 ∈ 𝑦 𝑧) |
| 175 | | uniiun 5058 |
. . . . . . . 8
⊢ ∪ 𝑦 =
∪ 𝑧 ∈ 𝑦 𝑧 |
| 176 | 174, 175 | eqtr4di 2795 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → ∪ 𝑧 ∈ 𝑦 (𝑋 ∖ (𝑋 ∖ 𝑧)) = ∪ 𝑦) |
| 177 | 171, 176 | eqtr3id 2791 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → (𝑋 ∖ ∩
𝑧 ∈ 𝑦 (𝑋 ∖ 𝑧)) = ∪ 𝑦) |
| 178 | 170, 177 | neeqtrd 3010 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) ∧ 𝑦 ≠ ∅) → 𝑋 ≠ ∪ 𝑦) |
| 179 | 11 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝐹 ∈ (Fil‘𝑋)) |
| 180 | | filtop 23863 |
. . . . . 6
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
| 181 | | fileln0 23858 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑋 ∈ 𝐹) → 𝑋 ≠ ∅) |
| 182 | 179, 180,
181 | syl2anc2 585 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝑋 ≠ ∅) |
| 183 | 121, 178,
182 | pm2.61ne 3027 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → 𝑋 ≠ ∪ 𝑦) |
| 184 | 183 | neneqd 2945 |
. . 3
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)) → ¬ 𝑋 = ∪ 𝑦) |
| 185 | 184 | nrexdv 3149 |
. 2
⊢ (𝜑 → ¬ ∃𝑦 ∈ (𝒫 (𝐵 ∖ 𝐹) ∩ Fin)𝑋 = ∪ 𝑦) |
| 186 | 117, 185 | pm2.65i 194 |
1
⊢ ¬
𝜑 |