Step | Hyp | Ref
| Expression |
1 | | filsspw 21465 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋) |
2 | | 0nelfil 21463 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → ¬ ∅ ∈
𝐹) |
3 | | filtop 21469 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝑋 ∈ 𝐹) |
4 | 1, 2, 3 | 3jca 1235 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹)) |
5 | | elpwi 4117 |
. . . . 5
⊢ (𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋) |
6 | | filss 21467 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥)) → 𝑥 ∈ 𝐹) |
7 | 6 | 3exp2 1277 |
. . . . . . . 8
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑦 ∈ 𝐹 → (𝑥 ⊆ 𝑋 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))) |
8 | 7 | com23 84 |
. . . . . . 7
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝑥 ⊆ 𝑋 → (𝑦 ∈ 𝐹 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)))) |
9 | 8 | imp 444 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑦 ∈ 𝐹 → (𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹))) |
10 | 9 | rexlimdv 3012 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)) |
11 | 5, 10 | sylan2 490 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝒫 𝑋) → (∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)) |
12 | 11 | ralrimiva 2949 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹)) |
13 | | filin 21468 |
. . . . 5
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
14 | 13 | 3expb 1258 |
. . . 4
⊢ ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
15 | 14 | ralrimivva 2954 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) |
16 | 4, 12, 15 | 3jca 1235 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → ((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹)) |
17 | | simp11 1084 |
. . . 4
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ⊆ 𝒫 𝑋) |
18 | | simp13 1086 |
. . . . . 6
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝑋 ∈ 𝐹) |
19 | | ne0i 3880 |
. . . . . 6
⊢ (𝑋 ∈ 𝐹 → 𝐹 ≠ ∅) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ≠ ∅) |
21 | | simp12 1085 |
. . . . . 6
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ¬ ∅ ∈ 𝐹) |
22 | | df-nel 2783 |
. . . . . 6
⊢ (∅
∉ 𝐹 ↔ ¬
∅ ∈ 𝐹) |
23 | 21, 22 | sylibr 223 |
. . . . 5
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ∅ ∉ 𝐹) |
24 | | ssid 3587 |
. . . . . . . . 9
⊢ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦) |
25 | | sseq1 3589 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑥 ∩ 𝑦) → (𝑧 ⊆ (𝑥 ∩ 𝑦) ↔ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦))) |
26 | 25 | rspcev 3282 |
. . . . . . . . 9
⊢ (((𝑥 ∩ 𝑦) ∈ 𝐹 ∧ (𝑥 ∩ 𝑦) ⊆ (𝑥 ∩ 𝑦)) → ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
27 | 24, 26 | mpan2 703 |
. . . . . . . 8
⊢ ((𝑥 ∩ 𝑦) ∈ 𝐹 → ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
28 | 27 | ralimi 2936 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹 → ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
29 | 28 | ralimi 2936 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹 → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
30 | 29 | 3ad2ant3 1077 |
. . . . 5
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦)) |
31 | 20, 23, 30 | 3jca 1235 |
. . . 4
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))) |
32 | | isfbas2 21449 |
. . . . 5
⊢ (𝑋 ∈ 𝐹 → (𝐹 ∈ (fBas‘𝑋) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
33 | 18, 32 | syl 17 |
. . . 4
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → (𝐹 ∈ (fBas‘𝑋) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 ∃𝑧 ∈ 𝐹 𝑧 ⊆ (𝑥 ∩ 𝑦))))) |
34 | 17, 31, 33 | mpbir2and 959 |
. . 3
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ∈ (fBas‘𝑋)) |
35 | | n0 3890 |
. . . . . . . 8
⊢ ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ ↔
∃𝑦 𝑦 ∈ (𝐹 ∩ 𝒫 𝑥)) |
36 | | elin 3758 |
. . . . . . . . . 10
⊢ (𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) ↔ (𝑦 ∈ 𝐹 ∧ 𝑦 ∈ 𝒫 𝑥)) |
37 | | elpwi 4117 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝒫 𝑥 → 𝑦 ⊆ 𝑥) |
38 | 37 | anim2i 591 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐹 ∧ 𝑦 ∈ 𝒫 𝑥) → (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
39 | 36, 38 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) → (𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
40 | 39 | eximi 1752 |
. . . . . . . 8
⊢
(∃𝑦 𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) → ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
41 | 35, 40 | sylbi 206 |
. . . . . . 7
⊢ ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ →
∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
42 | | df-rex 2902 |
. . . . . . 7
⊢
(∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑥 ↔ ∃𝑦(𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥)) |
43 | 41, 42 | sylibr 223 |
. . . . . 6
⊢ ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ →
∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥) |
44 | 43 | imim1i 61 |
. . . . 5
⊢
((∃𝑦 ∈
𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) → ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)) |
45 | 44 | ralimi 2936 |
. . . 4
⊢
(∀𝑥 ∈
𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) → ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)) |
46 | 45 | 3ad2ant2 1076 |
. . 3
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹)) |
47 | | isfil 21461 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥 ∈ 𝐹))) |
48 | 34, 46, 47 | sylanbrc 695 |
. 2
⊢ (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈
𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋)) |
49 | 16, 48 | impbii 198 |
1
⊢ (𝐹 ∈ (Fil‘𝑋) ↔ ((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹) ∧ ∀𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ 𝐹)) |