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 ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → { 𝐴 } ∈ ( 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 eqsbc1 ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑥 ] 𝑥 = 𝐴 ↔ 𝐴 = 𝐴 ) )
9 7 8 mpbiri ⊢ ( 𝐴 ∈ 𝐵 → [ 𝐴 / 𝑥 ] 𝑥 = 𝐴 )
10 9 adantr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → [ 𝐴 / 𝑥 ] 𝑥 = 𝐴 )
11 simpr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
12 11 necomd ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → ∅ ≠ 𝐴 )
13 12 neneqd ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → ¬ ∅ = 𝐴 )
14 0ex ⊢ ∅ ∈ V
15 eqsbc1 ⊢ ( ∅ ∈ V → ( [ ∅ / 𝑥 ] 𝑥 = 𝐴 ↔ ∅ = 𝐴 ) )
16 14 15 ax-mp ⊢ ( [ ∅ / 𝑥 ] 𝑥 = 𝐴 ↔ ∅ = 𝐴 )
17 13 16 sylnibr ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → ¬ [ ∅ / 𝑥 ] 𝑥 = 𝐴 )
18 sseq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝑦 ) )
19 18 anbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦 ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦 ) ) )
20 eqss ⊢ ( 𝑦 = 𝐴 ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦 ) )
21 20 biimpri ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ 𝑦 ) → 𝑦 = 𝐴 )
22 19 21 biimtrdi ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦 ) → 𝑦 = 𝐴 ) )
23 22 com12 ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 = 𝐴 → 𝑦 = 𝐴 ) )
24 23 3adant1 ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝑦 ) → ( 𝑥 = 𝐴 → 𝑦 = 𝐴 ) )
25 sbcid ⊢ ( [ 𝑥 / 𝑥 ] 𝑥 = 𝐴 ↔ 𝑥 = 𝐴 )
26 eqsbc1 ⊢ ( 𝑦 ∈ 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 eqsbc1 ⊢ ( ( 𝑦 ∩ 𝑥 ) ∈ V → ( [ ( 𝑦 ∩ 𝑥 ) / 𝑥 ] 𝑥 = 𝐴 ↔ ( 𝑦 ∩ 𝑥 ) = 𝐴 ) )
36 34 35 ax-mp ⊢ ( [ ( 𝑦 ∩ 𝑥 ) / 𝑥 ] 𝑥 = 𝐴 ↔ ( 𝑦 ∩ 𝑥 ) = 𝐴 )
37 32 36 sylibr ⊢ ( ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴 ∧ [ 𝑥 / 𝑥 ] 𝑥 = 𝐴 ) → [ ( 𝑦 ∩ 𝑥 ) / 𝑥 ] 𝑥 = 𝐴 )
38 37 a1i ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) ∧ 𝑦 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐴 ) → ( ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴 ∧ [ 𝑥 / 𝑥 ] 𝑥 = 𝐴 ) → [ ( 𝑦 ∩ 𝑥 ) / 𝑥 ] 𝑥 = 𝐴 ) )
39 5 6 10 17 28 38 isfild ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅ ) → { 𝐴 } ∈ ( Fil ‘ 𝐴 ) )