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 ‘ 𝐴 ) )