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