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

Theorem snfil 21420
Description: A singleton is a filter. Example 1 of [BourbakiTop1] p. I.36. (Contributed by FL, 16-Sep-2007.) (Revised by Stefan O'Rear, 2-Aug-2015.)
Assertion
Ref Expression
snfil ((𝐴𝐵𝐴 ≠ ∅) → {𝐴} ∈ (Fil‘𝐴))

Proof of Theorem snfil
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 velsn 4140 . . . 4 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2 eqimss 3619 . . . . 5 (𝑥 = 𝐴𝑥𝐴)
32pm4.71ri 662 . . . 4 (𝑥 = 𝐴 ↔ (𝑥𝐴𝑥 = 𝐴))
41, 3bitri 262 . . 3 (𝑥 ∈ {𝐴} ↔ (𝑥𝐴𝑥 = 𝐴))
54a1i 11 . 2 ((𝐴𝐵𝐴 ≠ ∅) → (𝑥 ∈ {𝐴} ↔ (𝑥𝐴𝑥 = 𝐴)))
6 elex 3184 . . 3 (𝐴𝐵𝐴 ∈ V)
76adantr 479 . 2 ((𝐴𝐵𝐴 ≠ ∅) → 𝐴 ∈ V)
8 eqid 2609 . . . 4 𝐴 = 𝐴
9 eqsbc3 3441 . . . 4 (𝐴𝐵 → ([𝐴 / 𝑥]𝑥 = 𝐴𝐴 = 𝐴))
108, 9mpbiri 246 . . 3 (𝐴𝐵[𝐴 / 𝑥]𝑥 = 𝐴)
1110adantr 479 . 2 ((𝐴𝐵𝐴 ≠ ∅) → [𝐴 / 𝑥]𝑥 = 𝐴)
12 simpr 475 . . . . 5 ((𝐴𝐵𝐴 ≠ ∅) → 𝐴 ≠ ∅)
1312necomd 2836 . . . 4 ((𝐴𝐵𝐴 ≠ ∅) → ∅ ≠ 𝐴)
1413neneqd 2786 . . 3 ((𝐴𝐵𝐴 ≠ ∅) → ¬ ∅ = 𝐴)
15 0ex 4713 . . . 4 ∅ ∈ V
16 eqsbc3 3441 . . . 4 (∅ ∈ V → ([∅ / 𝑥]𝑥 = 𝐴 ↔ ∅ = 𝐴))
1715, 16ax-mp 5 . . 3 ([∅ / 𝑥]𝑥 = 𝐴 ↔ ∅ = 𝐴)
1814, 17sylnibr 317 . 2 ((𝐴𝐵𝐴 ≠ ∅) → ¬ [∅ / 𝑥]𝑥 = 𝐴)
19 sseq1 3588 . . . . . . 7 (𝑥 = 𝐴 → (𝑥𝑦𝐴𝑦))
2019anbi2d 735 . . . . . 6 (𝑥 = 𝐴 → ((𝑦𝐴𝑥𝑦) ↔ (𝑦𝐴𝐴𝑦)))
21 eqss 3582 . . . . . . 7 (𝑦 = 𝐴 ↔ (𝑦𝐴𝐴𝑦))
2221biimpri 216 . . . . . 6 ((𝑦𝐴𝐴𝑦) → 𝑦 = 𝐴)
2320, 22syl6bi 241 . . . . 5 (𝑥 = 𝐴 → ((𝑦𝐴𝑥𝑦) → 𝑦 = 𝐴))
2423com12 32 . . . 4 ((𝑦𝐴𝑥𝑦) → (𝑥 = 𝐴𝑦 = 𝐴))
25243adant1 1071 . . 3 (((𝐴𝐵𝐴 ≠ ∅) ∧ 𝑦𝐴𝑥𝑦) → (𝑥 = 𝐴𝑦 = 𝐴))
26 sbcid 3418 . . 3 ([𝑥 / 𝑥]𝑥 = 𝐴𝑥 = 𝐴)
27 vex 3175 . . . 4 𝑦 ∈ V
28 eqsbc3 3441 . . . 4 (𝑦 ∈ V → ([𝑦 / 𝑥]𝑥 = 𝐴𝑦 = 𝐴))
2927, 28ax-mp 5 . . 3 ([𝑦 / 𝑥]𝑥 = 𝐴𝑦 = 𝐴)
3025, 26, 293imtr4g 283 . 2 (((𝐴𝐵𝐴 ≠ ∅) ∧ 𝑦𝐴𝑥𝑦) → ([𝑥 / 𝑥]𝑥 = 𝐴[𝑦 / 𝑥]𝑥 = 𝐴))
31 ineq12 3770 . . . . . 6 ((𝑦 = 𝐴𝑥 = 𝐴) → (𝑦𝑥) = (𝐴𝐴))
32 inidm 3783 . . . . . 6 (𝐴𝐴) = 𝐴
3331, 32syl6eq 2659 . . . . 5 ((𝑦 = 𝐴𝑥 = 𝐴) → (𝑦𝑥) = 𝐴)
3429, 26, 33syl2anb 494 . . . 4 (([𝑦 / 𝑥]𝑥 = 𝐴[𝑥 / 𝑥]𝑥 = 𝐴) → (𝑦𝑥) = 𝐴)
3527inex1 4722 . . . . 5 (𝑦𝑥) ∈ V
36 eqsbc3 3441 . . . . 5 ((𝑦𝑥) ∈ V → ([(𝑦𝑥) / 𝑥]𝑥 = 𝐴 ↔ (𝑦𝑥) = 𝐴))
3735, 36ax-mp 5 . . . 4 ([(𝑦𝑥) / 𝑥]𝑥 = 𝐴 ↔ (𝑦𝑥) = 𝐴)
3834, 37sylibr 222 . . 3 (([𝑦 / 𝑥]𝑥 = 𝐴[𝑥 / 𝑥]𝑥 = 𝐴) → [(𝑦𝑥) / 𝑥]𝑥 = 𝐴)
3938a1i 11 . 2 (((𝐴𝐵𝐴 ≠ ∅) ∧ 𝑦𝐴𝑥𝐴) → (([𝑦 / 𝑥]𝑥 = 𝐴[𝑥 / 𝑥]𝑥 = 𝐴) → [(𝑦𝑥) / 𝑥]𝑥 = 𝐴))
405, 7, 11, 18, 30, 39isfild 21414 1 ((𝐴𝐵𝐴 ≠ ∅) → {𝐴} ∈ (Fil‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  Vcvv 3172  [wsbc 3401  cin 3538  wss 3539  c0 3873  {csn 4124  cfv 5790  Filcfil 21401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fv 5798  df-fbas 19510  df-fil 21402
This theorem is referenced by:  snfbas  21422
  Copyright terms: Public domain W3C validator