| Step | Hyp | Ref
| Expression |
| 1 | | filsspw 23859 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋) |
| 2 | | 0nelfil 23857 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∅ ∈
𝐹) |
| 3 | | filtop 23863 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
| 4 | 1, 2, 3 | 3jca 1129 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹)) |
| 5 | | elpwi 4607 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
| 6 | | filss 23861 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝐹) |
| 7 | 6 | 3exp2 1355 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))) |
| 8 | 7 | com23 86 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ⊆ 𝑋 → (𝑦 ∈ 𝐹 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))) |
| 9 | 8 | imp 406 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑦 ∈ 𝐹 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹))) |
| 10 | 9 | rexlimdv 3153 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)) |
| 11 | 5, 10 | sylan2 593 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝒫 𝑋) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)) |
| 12 | 11 | ralrimiva 3146 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)) |
| 13 | | filin 23862 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
| 14 | 13 | 3expb 1121 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
| 15 | 14 | ralrimivva 3202 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) |
| 16 | 4, 12, 15 | 3jca 1129 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹)) |
| 17 | | simp11 1204 |
. . . 4
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ⊆ 𝒫 𝑋) |
| 18 | | simp13 1206 |
. . . . . 6
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝑋 ∈ 𝐹) |
| 19 | 18 | ne0d 4342 |
. . . . 5
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ≠ ∅) |
| 20 | | simp12 1205 |
. . . . . 6
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ¬ ∅ ∈ 𝐹) |
| 21 | | df-nel 3047 |
. . . . . 6
⊢ (∅
∉ 𝐹 ↔ ¬
∅ ∈ 𝐹) |
| 22 | 20, 21 | sylibr 234 |
. . . . 5
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ∅ ∉ 𝐹) |
| 23 | | ssid 4006 |
. . . . . . . . 9
⊢ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦) |
| 24 | | sseq1 4009 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑥 ∩ 𝑦) → (𝑧 ⊆ (𝑥 ∩ 𝑦) ↔ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦))) |
| 25 | 24 | rspcev 3622 |
. . . . . . . . 9
⊢ (((𝑥 ∩ 𝑦) ∈ 𝐹 ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦)) → ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
| 26 | 23, 25 | mpan2 691 |
. . . . . . . 8
⊢ ((𝑥 ∩ 𝑦) ∈ 𝐹 → ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
| 27 | 26 | ralimi 3083 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹 → ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
| 28 | 27 | ralimi 3083 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹 → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
| 29 | 28 | 3ad2ant3 1136 |
. . . . 5
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
| 30 | 19, 22, 29 | 3jca 1129 |
. . . 4
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))) |
| 31 | | isfbas2 23843 |
. . . . 5
⊢ (𝑋 ∈ 𝐹 → (𝐹 ∈ (fBas‘𝑋) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
| 32 | 18, 31 | syl 17 |
. . . 4
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → (𝐹 ∈ (fBas‘𝑋) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
| 33 | 17, 30, 32 | mpbir2and 713 |
. . 3
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ∈ (fBas‘𝑋)) |
| 34 | | n0 4353 |
. . . . . . . 8
⊢ ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ ↔
∃𝑦 𝑦 ∈ (𝐹 ∩ 𝒫 𝑥)) |
| 35 | | elin 3967 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) ↔ (𝑦 ∈ 𝐹 ∧ 𝑦 ∈ 𝒫 𝑥)) |
| 36 | | elpwi 4607 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 𝑥 → 𝑦 ⊆ 𝑥) |
| 37 | 36 | anim2i 617 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 ∈ 𝒫 𝑥) → (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
| 38 | 35, 37 | sylbi 217 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) → (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
| 39 | 38 | eximi 1835 |
. . . . . . . 8
⊢
(∃𝑦 𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
| 40 | 34, 39 | sylbi 217 |
. . . . . . 7
⊢ ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ →
∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
| 41 | | df-rex 3071 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑥 ↔ ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
| 42 | 40, 41 | sylibr 234 |
. . . . . 6
⊢ ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ →
∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥) |
| 43 | 42 | imim1i 63 |
. . . . 5
⊢
((∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) → ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)) |
| 44 | 43 | ralimi 3083 |
. . . 4
⊢
(∀𝑥 ∈
𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) → ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)) |
| 45 | 44 | 3ad2ant2 1135 |
. . 3
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)) |
| 46 | | isfil 23855 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹))) |
| 47 | 33, 45, 46 | sylanbrc 583 |
. 2
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋)) |
| 48 | 16, 47 | impbii 209 |
1
⊢ (𝐹 ∈ (Fil‘𝑋) ↔ ((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹)) |