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 ( ( 𝐴𝐵𝐴 ≠ ∅ ) → { 𝐴 } ∈ ( Fil ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 velsn ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
2 eqimss ( 𝑥 = 𝐴𝑥𝐴 )
3 2 pm4.71ri ( 𝑥 = 𝐴 ↔ ( 𝑥𝐴𝑥 = 𝐴 ) )
4 1 3 bitri ( 𝑥 ∈ { 𝐴 } ↔ ( 𝑥𝐴𝑥 = 𝐴 ) )
5 4 a1i ( ( 𝐴𝐵𝐴 ≠ ∅ ) → ( 𝑥 ∈ { 𝐴 } ↔ ( 𝑥𝐴𝑥 = 𝐴 ) ) )
6 simpl ( ( 𝐴𝐵𝐴 ≠ ∅ ) → 𝐴𝐵 )
7 eqid 𝐴 = 𝐴
8 eqsbc3 ( 𝐴𝐵 → ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐴𝐴 = 𝐴 ) )
9 7 8 mpbiri ( 𝐴𝐵[ 𝐴 / 𝑥 ] 𝑥 = 𝐴 )
10 9 adantr ( ( 𝐴𝐵𝐴 ≠ ∅ ) → [ 𝐴 / 𝑥 ] 𝑥 = 𝐴 )
11 simpr ( ( 𝐴𝐵𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
12 11 necomd ( ( 𝐴𝐵𝐴 ≠ ∅ ) → ∅ ≠ 𝐴 )
13 12 neneqd ( ( 𝐴𝐵𝐴 ≠ ∅ ) → ¬ ∅ = 𝐴 )
14 0ex ∅ ∈ V
15 eqsbc3 ( ∅ ∈ V → ( [ ∅ / 𝑥 ] 𝑥 = 𝐴 ↔ ∅ = 𝐴 ) )
16 14 15 ax-mp ( [ ∅ / 𝑥 ] 𝑥 = 𝐴 ↔ ∅ = 𝐴 )
17 13 16 sylnibr ( ( 𝐴𝐵𝐴 ≠ ∅ ) → ¬ [ ∅ / 𝑥 ] 𝑥 = 𝐴 )
18 sseq1 ( 𝑥 = 𝐴 → ( 𝑥𝑦𝐴𝑦 ) )
19 18 anbi2d ( 𝑥 = 𝐴 → ( ( 𝑦𝐴𝑥𝑦 ) ↔ ( 𝑦𝐴𝐴𝑦 ) ) )
20 eqss ( 𝑦 = 𝐴 ↔ ( 𝑦𝐴𝐴𝑦 ) )
21 20 biimpri ( ( 𝑦𝐴𝐴𝑦 ) → 𝑦 = 𝐴 )
22 19 21 syl6bi ( 𝑥 = 𝐴 → ( ( 𝑦𝐴𝑥𝑦 ) → 𝑦 = 𝐴 ) )
23 22 com12 ( ( 𝑦𝐴𝑥𝑦 ) → ( 𝑥 = 𝐴𝑦 = 𝐴 ) )
24 23 3adant1 ( ( ( 𝐴𝐵𝐴 ≠ ∅ ) ∧ 𝑦𝐴𝑥𝑦 ) → ( 𝑥 = 𝐴𝑦 = 𝐴 ) )
25 sbcid ( [ 𝑥 / 𝑥 ] 𝑥 = 𝐴𝑥 = 𝐴 )
26 eqsbc3 ( 𝑦 ∈ V → ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴𝑦 = 𝐴 ) )
27 26 elv ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴𝑦 = 𝐴 )
28 24 25 27 3imtr4g ( ( ( 𝐴𝐵𝐴 ≠ ∅ ) ∧ 𝑦𝐴𝑥𝑦 ) → ( [ 𝑥 / 𝑥 ] 𝑥 = 𝐴[ 𝑦 / 𝑥 ] 𝑥 = 𝐴 ) )
29 ineq12 ( ( 𝑦 = 𝐴𝑥 = 𝐴 ) → ( 𝑦𝑥 ) = ( 𝐴𝐴 ) )
30 inidm ( 𝐴𝐴 ) = 𝐴
31 29 30 eqtrdi ( ( 𝑦 = 𝐴𝑥 = 𝐴 ) → ( 𝑦𝑥 ) = 𝐴 )
32 27 25 31 syl2anb ( ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴[ 𝑥 / 𝑥 ] 𝑥 = 𝐴 ) → ( 𝑦𝑥 ) = 𝐴 )
33 vex 𝑦 ∈ V
34 33 inex1 ( 𝑦𝑥 ) ∈ V
35 eqsbc3 ( ( 𝑦𝑥 ) ∈ V → ( [ ( 𝑦𝑥 ) / 𝑥 ] 𝑥 = 𝐴 ↔ ( 𝑦𝑥 ) = 𝐴 ) )
36 34 35 ax-mp ( [ ( 𝑦𝑥 ) / 𝑥 ] 𝑥 = 𝐴 ↔ ( 𝑦𝑥 ) = 𝐴 )
37 32 36 sylibr ( ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴[ 𝑥 / 𝑥 ] 𝑥 = 𝐴 ) → [ ( 𝑦𝑥 ) / 𝑥 ] 𝑥 = 𝐴 )
38 37 a1i ( ( ( 𝐴𝐵𝐴 ≠ ∅ ) ∧ 𝑦𝐴𝑥𝐴 ) → ( ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴[ 𝑥 / 𝑥 ] 𝑥 = 𝐴 ) → [ ( 𝑦𝑥 ) / 𝑥 ] 𝑥 = 𝐴 ) )
39 5 6 10 17 28 38 isfild ( ( 𝐴𝐵𝐴 ≠ ∅ ) → { 𝐴 } ∈ ( Fil ‘ 𝐴 ) )