This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 eqsbc1 
 |-  ( 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 eqsbc1 
 |-  ( (/) 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 biimtrdi 
 |-  ( 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 eqsbc1 
 |-  ( 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 eqsbc1 
 |-  ( ( 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 ) )