Step | Hyp | Ref
| Expression |
1 | | filsspw 22748 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋) |
2 | | 0nelfil 22746 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∅ ∈
𝐹) |
3 | | filtop 22752 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
4 | 1, 2, 3 | 3jca 1130 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹)) |
5 | | elpwi 4522 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
6 | | filss 22750 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝐹) |
7 | 6 | 3exp2 1356 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))) |
8 | 7 | com23 86 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ⊆ 𝑋 → (𝑦 ∈ 𝐹 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))) |
9 | 8 | imp 410 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑦 ∈ 𝐹 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹))) |
10 | 9 | rexlimdv 3202 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)) |
11 | 5, 10 | sylan2 596 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝒫 𝑋) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)) |
12 | 11 | ralrimiva 3105 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)) |
13 | | filin 22751 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
14 | 13 | 3expb 1122 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
15 | 14 | ralrimivva 3112 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) |
16 | 4, 12, 15 | 3jca 1130 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹)) |
17 | | simp11 1205 |
. . . 4
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ⊆ 𝒫 𝑋) |
18 | | simp13 1207 |
. . . . . 6
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝑋 ∈ 𝐹) |
19 | 18 | ne0d 4250 |
. . . . 5
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ≠ ∅) |
20 | | simp12 1206 |
. . . . . 6
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ¬ ∅ ∈ 𝐹) |
21 | | df-nel 3047 |
. . . . . 6
⊢ (∅
∉ 𝐹 ↔ ¬
∅ ∈ 𝐹) |
22 | 20, 21 | sylibr 237 |
. . . . 5
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ∅ ∉ 𝐹) |
23 | | ssid 3923 |
. . . . . . . . 9
⊢ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦) |
24 | | sseq1 3926 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑥 ∩ 𝑦) → (𝑧 ⊆ (𝑥 ∩ 𝑦) ↔ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦))) |
25 | 24 | rspcev 3537 |
. . . . . . . . 9
⊢ (((𝑥 ∩ 𝑦) ∈ 𝐹 ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦)) → ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
26 | 23, 25 | mpan2 691 |
. . . . . . . 8
⊢ ((𝑥 ∩ 𝑦) ∈ 𝐹 → ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
27 | 26 | ralimi 3083 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹 → ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
28 | 27 | ralimi 3083 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹 → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
29 | 28 | 3ad2ant3 1137 |
. . . . 5
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
30 | 19, 22, 29 | 3jca 1130 |
. . . 4
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))) |
31 | | isfbas2 22732 |
. . . . 5
⊢ (𝑋 ∈ 𝐹 → (𝐹 ∈ (fBas‘𝑋) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
32 | 18, 31 | syl 17 |
. . . 4
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → (𝐹 ∈ (fBas‘𝑋) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
33 | 17, 30, 32 | mpbir2and 713 |
. . 3
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ∈ (fBas‘𝑋)) |
34 | | n0 4261 |
. . . . . . . 8
⊢ ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ ↔
∃𝑦 𝑦 ∈ (𝐹 ∩ 𝒫 𝑥)) |
35 | | elin 3882 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) ↔ (𝑦 ∈ 𝐹 ∧ 𝑦 ∈ 𝒫 𝑥)) |
36 | | elpwi 4522 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 𝑥 → 𝑦 ⊆ 𝑥) |
37 | 36 | anim2i 620 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 ∈ 𝒫 𝑥) → (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
38 | 35, 37 | sylbi 220 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) → (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
39 | 38 | eximi 1842 |
. . . . . . . 8
⊢
(∃𝑦 𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
40 | 34, 39 | sylbi 220 |
. . . . . . 7
⊢ ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ →
∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
41 | | df-rex 3067 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑥 ↔ ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
42 | 40, 41 | sylibr 237 |
. . . . . 6
⊢ ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ →
∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥) |
43 | 42 | imim1i 63 |
. . . . 5
⊢
((∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) → ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)) |
44 | 43 | ralimi 3083 |
. . . 4
⊢
(∀𝑥 ∈
𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) → ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)) |
45 | 44 | 3ad2ant2 1136 |
. . 3
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)) |
46 | | isfil 22744 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹))) |
47 | 33, 45, 46 | sylanbrc 586 |
. 2
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋)) |
48 | 16, 47 | impbii 212 |
1
⊢ (𝐹 ∈ (Fil‘𝑋) ↔ ((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹)) |