Metamath Proof Explorer

Theorem isfil2

Description: Derive the standard axioms of a filter. (Contributed by Mario Carneiro, 27-Nov-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion isfil2 ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ↔ ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 filsspw ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ⊆ 𝒫 𝑋 )
2 0nelfil ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ¬ ∅ ∈ 𝐹 )
3 filtop ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ 𝐹 )
4 1 2 3 3jca ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) )
5 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑋 → 𝑥 ⊆ 𝑋 )
6 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑦 ∈ 𝐹 ∧ 𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑥 ) ) → 𝑥 ∈ 𝐹 )
7 6 3exp2 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑦 ∈ 𝐹 → ( 𝑥 ⊆ 𝑋 → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ) ) )
8 7 com23 ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝑥 ⊆ 𝑋 → ( 𝑦 ∈ 𝐹 → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ) ) )
9 8 imp ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑦 ∈ 𝐹 → ( 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ) )
10 9 rexlimdv ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) )
11 5 10 sylan2 ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) )
12 11 ralrimiva ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) )
13 filin ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
14 13 3expb ⊢ ( ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
15 14 ralrimivva ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
16 4 12 15 3jca ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) )
17 simp11 ⊢ ( ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) → 𝐹 ⊆ 𝒫 𝑋 )
18 simp13 ⊢ ( ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) → 𝑋 ∈ 𝐹 )
19 18 ne0d ⊢ ( ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) → 𝐹 ≠ ∅ )
20 simp12 ⊢ ( ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) → ¬ ∅ ∈ 𝐹 )
21 df-nel ⊢ ( ∅ ∉ 𝐹 ↔ ¬ ∅ ∈ 𝐹 )
22 20 21 sylibr ⊢ ( ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) → ∅ ∉ 𝐹 )
23 ssid ⊢ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 )
24 sseq1 ⊢ ( 𝑧 = ( 𝑥 ∩ 𝑦 ) → ( 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ↔ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) )
25 24 rspcev ⊢ ( ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ∧ ( 𝑥 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
26 23 25 mpan2 ⊢ ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 → ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
27 26 ralimi ⊢ ( ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 → ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
28 27 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 → ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
29 28 3ad2ant3 ⊢ ( ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) → ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) )
30 19 22 29 3jca ⊢ ( ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) → ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) )
31 isfbas2 ⊢ ( 𝑋 ∈ 𝐹 → ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
32 18 31 syl ⊢ ( ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) → ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ↔ ( 𝐹 ⊆ 𝒫 𝑋 ∧ ( 𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ∃ 𝑧 ∈ 𝐹 𝑧 ⊆ ( 𝑥 ∩ 𝑦 ) ) ) ) )
33 17 30 32 mpbir2and ⊢ ( ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
34 n0 ⊢ ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ ( 𝐹 ∩ 𝒫 𝑥 ) )
35 elin ⊢ ( 𝑦 ∈ ( 𝐹 ∩ 𝒫 𝑥 ) ↔ ( 𝑦 ∈ 𝐹 ∧ 𝑦 ∈ 𝒫 𝑥 ) )
36 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑥 → 𝑦 ⊆ 𝑥 )
37 36 anim2i ⊢ ( ( 𝑦 ∈ 𝐹 ∧ 𝑦 ∈ 𝒫 𝑥 ) → ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) )
38 35 37 sylbi ⊢ ( 𝑦 ∈ ( 𝐹 ∩ 𝒫 𝑥 ) → ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) )
39 38 eximi ⊢ ( ∃ 𝑦 𝑦 ∈ ( 𝐹 ∩ 𝒫 𝑥 ) → ∃ 𝑦 ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) )
40 34 39 sylbi ⊢ ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ → ∃ 𝑦 ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) )
41 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐹 ∧ 𝑦 ⊆ 𝑥 ) )
42 40 41 sylibr ⊢ ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ → ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 )
43 42 imim1i ⊢ ( ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) → ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) )
44 43 ralimi ⊢ ( ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) → ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) )
45 44 3ad2ant2 ⊢ ( ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) → ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) )
46 isfil ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ → 𝑥 ∈ 𝐹 ) ) )
47 33 45 46 sylanbrc ⊢ ( ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
48 16 47 impbii ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ↔ ( ( 𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹 ∧ 𝑋 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( ∃ 𝑦 ∈ 𝐹 𝑦 ⊆ 𝑥 → 𝑥 ∈ 𝐹 ) ∧ ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 ) )