MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isfil2 Structured version   Visualization version   GIF version

Theorem isfil2 21873
Description: Derive the standard axioms of a filter. (Contributed by Mario Carneiro, 27-Nov-2013.) (Revised by Stefan O'Rear, 2-Aug-2015.)
Assertion
Ref Expression
isfil2 (𝐹 ∈ (Fil‘𝑋) ↔ ((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹))
Distinct variable groups:   𝑥,𝐹,𝑦   𝑥,𝑋,𝑦

Proof of Theorem isfil2
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 filsspw 21868 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝐹 ⊆ 𝒫 𝑋)
2 0nelfil 21866 . . . 4 (𝐹 ∈ (Fil‘𝑋) → ¬ ∅ ∈ 𝐹)
3 filtop 21872 . . . 4 (𝐹 ∈ (Fil‘𝑋) → 𝑋𝐹)
41, 2, 33jca 1122 . . 3 (𝐹 ∈ (Fil‘𝑋) → (𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹))
5 elpwi 4307 . . . . 5 (𝑥 ∈ 𝒫 𝑋𝑥𝑋)
6 filss 21870 . . . . . . . . 9 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑦𝐹𝑥𝑋𝑦𝑥)) → 𝑥𝐹)
763exp2 1447 . . . . . . . 8 (𝐹 ∈ (Fil‘𝑋) → (𝑦𝐹 → (𝑥𝑋 → (𝑦𝑥𝑥𝐹))))
87com23 86 . . . . . . 7 (𝐹 ∈ (Fil‘𝑋) → (𝑥𝑋 → (𝑦𝐹 → (𝑦𝑥𝑥𝐹))))
98imp 393 . . . . . 6 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → (𝑦𝐹 → (𝑦𝑥𝑥𝐹)))
109rexlimdv 3178 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝑋) → (∃𝑦𝐹 𝑦𝑥𝑥𝐹))
115, 10sylan2 580 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥 ∈ 𝒫 𝑋) → (∃𝑦𝐹 𝑦𝑥𝑥𝐹))
1211ralrimiva 3115 . . 3 (𝐹 ∈ (Fil‘𝑋) → ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹))
13 filin 21871 . . . . 5 ((𝐹 ∈ (Fil‘𝑋) ∧ 𝑥𝐹𝑦𝐹) → (𝑥𝑦) ∈ 𝐹)
14133expb 1113 . . . 4 ((𝐹 ∈ (Fil‘𝑋) ∧ (𝑥𝐹𝑦𝐹)) → (𝑥𝑦) ∈ 𝐹)
1514ralrimivva 3120 . . 3 (𝐹 ∈ (Fil‘𝑋) → ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹)
164, 12, 153jca 1122 . 2 (𝐹 ∈ (Fil‘𝑋) → ((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹))
17 simp11 1245 . . . 4 (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹) → 𝐹 ⊆ 𝒫 𝑋)
18 simp13 1247 . . . . . 6 (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹) → 𝑋𝐹)
19 ne0i 4069 . . . . . 6 (𝑋𝐹𝐹 ≠ ∅)
2018, 19syl 17 . . . . 5 (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹) → 𝐹 ≠ ∅)
21 simp12 1246 . . . . . 6 (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹) → ¬ ∅ ∈ 𝐹)
22 df-nel 3047 . . . . . 6 (∅ ∉ 𝐹 ↔ ¬ ∅ ∈ 𝐹)
2321, 22sylibr 224 . . . . 5 (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹) → ∅ ∉ 𝐹)
24 ssid 3773 . . . . . . . . 9 (𝑥𝑦) ⊆ (𝑥𝑦)
25 sseq1 3775 . . . . . . . . . 10 (𝑧 = (𝑥𝑦) → (𝑧 ⊆ (𝑥𝑦) ↔ (𝑥𝑦) ⊆ (𝑥𝑦)))
2625rspcev 3460 . . . . . . . . 9 (((𝑥𝑦) ∈ 𝐹 ∧ (𝑥𝑦) ⊆ (𝑥𝑦)) → ∃𝑧𝐹 𝑧 ⊆ (𝑥𝑦))
2724, 26mpan2 671 . . . . . . . 8 ((𝑥𝑦) ∈ 𝐹 → ∃𝑧𝐹 𝑧 ⊆ (𝑥𝑦))
2827ralimi 3101 . . . . . . 7 (∀𝑦𝐹 (𝑥𝑦) ∈ 𝐹 → ∀𝑦𝐹𝑧𝐹 𝑧 ⊆ (𝑥𝑦))
2928ralimi 3101 . . . . . 6 (∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹 → ∀𝑥𝐹𝑦𝐹𝑧𝐹 𝑧 ⊆ (𝑥𝑦))
30293ad2ant3 1129 . . . . 5 (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹) → ∀𝑥𝐹𝑦𝐹𝑧𝐹 𝑧 ⊆ (𝑥𝑦))
3120, 23, 303jca 1122 . . . 4 (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹) → (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥𝐹𝑦𝐹𝑧𝐹 𝑧 ⊆ (𝑥𝑦)))
32 isfbas2 21852 . . . . 5 (𝑋𝐹 → (𝐹 ∈ (fBas‘𝑋) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥𝐹𝑦𝐹𝑧𝐹 𝑧 ⊆ (𝑥𝑦)))))
3318, 32syl 17 . . . 4 (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹) → (𝐹 ∈ (fBas‘𝑋) ↔ (𝐹 ⊆ 𝒫 𝑋 ∧ (𝐹 ≠ ∅ ∧ ∅ ∉ 𝐹 ∧ ∀𝑥𝐹𝑦𝐹𝑧𝐹 𝑧 ⊆ (𝑥𝑦)))))
3417, 31, 33mpbir2and 692 . . 3 (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹) → 𝐹 ∈ (fBas‘𝑋))
35 n0 4078 . . . . . . . 8 ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ ↔ ∃𝑦 𝑦 ∈ (𝐹 ∩ 𝒫 𝑥))
36 elin 3947 . . . . . . . . . 10 (𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) ↔ (𝑦𝐹𝑦 ∈ 𝒫 𝑥))
37 elpwi 4307 . . . . . . . . . . 11 (𝑦 ∈ 𝒫 𝑥𝑦𝑥)
3837anim2i 603 . . . . . . . . . 10 ((𝑦𝐹𝑦 ∈ 𝒫 𝑥) → (𝑦𝐹𝑦𝑥))
3936, 38sylbi 207 . . . . . . . . 9 (𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) → (𝑦𝐹𝑦𝑥))
4039eximi 1910 . . . . . . . 8 (∃𝑦 𝑦 ∈ (𝐹 ∩ 𝒫 𝑥) → ∃𝑦(𝑦𝐹𝑦𝑥))
4135, 40sylbi 207 . . . . . . 7 ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → ∃𝑦(𝑦𝐹𝑦𝑥))
42 df-rex 3067 . . . . . . 7 (∃𝑦𝐹 𝑦𝑥 ↔ ∃𝑦(𝑦𝐹𝑦𝑥))
4341, 42sylibr 224 . . . . . 6 ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → ∃𝑦𝐹 𝑦𝑥)
4443imim1i 63 . . . . 5 ((∃𝑦𝐹 𝑦𝑥𝑥𝐹) → ((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝐹))
4544ralimi 3101 . . . 4 (∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) → ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝐹))
46453ad2ant2 1128 . . 3 (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹) → ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝐹))
47 isfil 21864 . . 3 (𝐹 ∈ (Fil‘𝑋) ↔ (𝐹 ∈ (fBas‘𝑋) ∧ ∀𝑥 ∈ 𝒫 𝑋((𝐹 ∩ 𝒫 𝑥) ≠ ∅ → 𝑥𝐹)))
4834, 46, 47sylanbrc 572 . 2 (((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹) → 𝐹 ∈ (Fil‘𝑋))
4916, 48impbii 199 1 (𝐹 ∈ (Fil‘𝑋) ↔ ((𝐹 ⊆ 𝒫 𝑋 ∧ ¬ ∅ ∈ 𝐹𝑋𝐹) ∧ ∀𝑥 ∈ 𝒫 𝑋(∃𝑦𝐹 𝑦𝑥𝑥𝐹) ∧ ∀𝑥𝐹𝑦𝐹 (𝑥𝑦) ∈ 𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071  wex 1852  wcel 2145  wne 2943  wnel 3046  wral 3061  wrex 3062  cin 3722  wss 3723  c0 4063  𝒫 cpw 4297  cfv 6029  fBascfbas 19942  Filcfil 21862
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5992  df-fun 6031  df-fv 6037  df-fbas 19951  df-fil 21863
This theorem is referenced by:  isfild  21875  infil  21880  neifil  21897  trfil2  21904
  Copyright terms: Public domain W3C validator