Metamath Proof Explorer


Theorem snfil

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)

Ref Expression
Assertion snfil
|- ( ( A e. B /\ A =/= (/) ) -> { A } e. ( Fil ` A ) )

Proof

Step Hyp Ref Expression
1 velsn
 |-  ( x e. { A } <-> x = A )
2 eqimss
 |-  ( x = A -> x C_ A )
3 2 pm4.71ri
 |-  ( x = A <-> ( x C_ A /\ x = A ) )
4 1 3 bitri
 |-  ( x e. { A } <-> ( x C_ A /\ x = A ) )
5 4 a1i
 |-  ( ( A e. B /\ A =/= (/) ) -> ( x e. { A } <-> ( x C_ A /\ x = A ) ) )
6 simpl
 |-  ( ( A e. B /\ A =/= (/) ) -> A e. B )
7 eqid
 |-  A = A
8 eqsbc3
 |-  ( A e. B -> ( [. A / x ]. x = A <-> A = A ) )
9 7 8 mpbiri
 |-  ( A e. B -> [. A / x ]. x = A )
10 9 adantr
 |-  ( ( A e. B /\ A =/= (/) ) -> [. A / x ]. x = A )
11 simpr
 |-  ( ( A e. B /\ A =/= (/) ) -> A =/= (/) )
12 11 necomd
 |-  ( ( A e. B /\ A =/= (/) ) -> (/) =/= A )
13 12 neneqd
 |-  ( ( A e. B /\ A =/= (/) ) -> -. (/) = A )
14 0ex
 |-  (/) e. _V
15 eqsbc3
 |-  ( (/) e. _V -> ( [. (/) / x ]. x = A <-> (/) = A ) )
16 14 15 ax-mp
 |-  ( [. (/) / x ]. x = A <-> (/) = A )
17 13 16 sylnibr
 |-  ( ( A e. B /\ A =/= (/) ) -> -. [. (/) / x ]. x = A )
18 sseq1
 |-  ( x = A -> ( x C_ y <-> A C_ y ) )
19 18 anbi2d
 |-  ( x = A -> ( ( y C_ A /\ x C_ y ) <-> ( y C_ A /\ A C_ y ) ) )
20 eqss
 |-  ( y = A <-> ( y C_ A /\ A C_ y ) )
21 20 biimpri
 |-  ( ( y C_ A /\ A C_ y ) -> y = A )
22 19 21 syl6bi
 |-  ( x = A -> ( ( y C_ A /\ x C_ y ) -> y = A ) )
23 22 com12
 |-  ( ( y C_ A /\ x C_ y ) -> ( x = A -> y = A ) )
24 23 3adant1
 |-  ( ( ( A e. B /\ A =/= (/) ) /\ y C_ A /\ x C_ y ) -> ( x = A -> y = A ) )
25 sbcid
 |-  ( [. x / x ]. x = A <-> x = A )
26 eqsbc3
 |-  ( y e. _V -> ( [. y / x ]. x = A <-> y = A ) )
27 26 elv
 |-  ( [. y / x ]. x = A <-> y = A )
28 24 25 27 3imtr4g
 |-  ( ( ( A e. B /\ A =/= (/) ) /\ y C_ A /\ x C_ y ) -> ( [. x / x ]. x = A -> [. y / x ]. x = A ) )
29 ineq12
 |-  ( ( y = A /\ x = A ) -> ( y i^i x ) = ( A i^i A ) )
30 inidm
 |-  ( A i^i A ) = A
31 29 30 eqtrdi
 |-  ( ( y = A /\ x = A ) -> ( y i^i x ) = A )
32 27 25 31 syl2anb
 |-  ( ( [. y / x ]. x = A /\ [. x / x ]. x = A ) -> ( y i^i x ) = A )
33 vex
 |-  y e. _V
34 33 inex1
 |-  ( y i^i x ) e. _V
35 eqsbc3
 |-  ( ( y i^i x ) e. _V -> ( [. ( y i^i x ) / x ]. x = A <-> ( y i^i x ) = A ) )
36 34 35 ax-mp
 |-  ( [. ( y i^i x ) / x ]. x = A <-> ( y i^i x ) = A )
37 32 36 sylibr
 |-  ( ( [. y / x ]. x = A /\ [. x / x ]. x = A ) -> [. ( y i^i x ) / x ]. x = A )
38 37 a1i
 |-  ( ( ( A e. B /\ A =/= (/) ) /\ y C_ A /\ x C_ A ) -> ( ( [. y / x ]. x = A /\ [. x / x ]. x = A ) -> [. ( y i^i x ) / x ]. x = A ) )
39 5 6 10 17 28 38 isfild
 |-  ( ( A e. B /\ A =/= (/) ) -> { A } e. ( Fil ` A ) )