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	$$⊢\left(A\in B\wedge A\ne \varnothing \right)\to \left\{A\right\}\in \mathrm{Fil}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
2		eqimss	$$⊢x=A\to x\subseteq A$$
3	2	pm4.71ri	$$⊢x=A\leftrightarrow \left(x\subseteq A\wedge x=A\right)$$
4	1 3	bitri	$$⊢x\in \left\{A\right\}\leftrightarrow \left(x\subseteq A\wedge x=A\right)$$
5	4	a1i	$$⊢\left(A\in B\wedge A\ne \varnothing \right)\to \left(x\in \left\{A\right\}\leftrightarrow \left(x\subseteq A\wedge x=A\right)\right)$$
6		simpl	$$⊢\left(A\in B\wedge A\ne \varnothing \right)\to A\in B$$
7		eqid	$$⊢A=A$$
8		eqsbc1	$$⊢A\in B\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}x=A\leftrightarrow A=A\right)$$
9	7 8	mpbiri	$$⊢A\in B\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}x=A$$
10	9	adantr	$$⊢\left(A\in B\wedge A\ne \varnothing \right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}x=A$$
11		simpr	$$⊢\left(A\in B\wedge A\ne \varnothing \right)\to A\ne \varnothing$$
12	11	necomd	$$⊢\left(A\in B\wedge A\ne \varnothing \right)\to \varnothing \ne A$$
13	12	neneqd	$$⊢\left(A\in B\wedge A\ne \varnothing \right)\to \neg \varnothing =A$$
14		0ex	$$⊢\varnothing \in \mathrm{V}$$
15		eqsbc1	$$⊢\varnothing \in \mathrm{V}\to \left(\underset{\dot{}}{[}\varnothing /x\underset{\dot{}}{]}x=A\leftrightarrow \varnothing =A\right)$$
16	14 15	ax-mp	$$⊢\underset{\dot{}}{[}\varnothing /x\underset{\dot{}}{]}x=A\leftrightarrow \varnothing =A$$
17	13 16	sylnibr	$$⊢\left(A\in B\wedge A\ne \varnothing \right)\to \neg \underset{\dot{}}{[}\varnothing /x\underset{\dot{}}{]}x=A$$
18		sseq1	$$⊢x=A\to \left(x\subseteq y\leftrightarrow A\subseteq y\right)$$
19	18	anbi2d	$$⊢x=A\to \left(\left(y\subseteq A\wedge x\subseteq y\right)\leftrightarrow \left(y\subseteq A\wedge A\subseteq y\right)\right)$$
20		eqss	$$⊢y=A\leftrightarrow \left(y\subseteq A\wedge A\subseteq y\right)$$
21	20	biimpri	$$⊢\left(y\subseteq A\wedge A\subseteq y\right)\to y=A$$
22	19 21	biimtrdi	$$⊢x=A\to \left(\left(y\subseteq A\wedge x\subseteq y\right)\to y=A\right)$$
23	22	com12	$$⊢\left(y\subseteq A\wedge x\subseteq y\right)\to \left(x=A\to y=A\right)$$
24	23	3adant1	$$⊢\left(\left(A\in B\wedge A\ne \varnothing \right)\wedge y\subseteq A\wedge x\subseteq y\right)\to \left(x=A\to y=A\right)$$
25		sbcid	$$⊢\underset{\dot{}}{[}x/x\underset{\dot{}}{]}x=A\leftrightarrow x=A$$
26		eqsbc1	$$⊢y\in \mathrm{V}\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}x=A\leftrightarrow y=A\right)$$
27	26	elv	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}x=A\leftrightarrow y=A$$
28	24 25 27	3imtr4g	$$⊢\left(\left(A\in B\wedge A\ne \varnothing \right)\wedge y\subseteq A\wedge x\subseteq y\right)\to \left(\underset{\dot{}}{[}x/x\underset{\dot{}}{]}x=A\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}x=A\right)$$
29		ineq12	$$⊢\left(y=A\wedge x=A\right)\to y\cap x=A\cap A$$
30		inidm	$$⊢A\cap A=A$$
31	29 30	eqtrdi	$$⊢\left(y=A\wedge x=A\right)\to y\cap x=A$$
32	27 25 31	syl2anb	$$⊢\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}x=A\wedge \underset{\dot{}}{[}x/x\underset{\dot{}}{]}x=A\right)\to y\cap x=A$$
33		vex	$$⊢y\in \mathrm{V}$$
34	33	inex1	$$⊢y\cap x\in \mathrm{V}$$
35		eqsbc1	$$⊢y\cap x\in \mathrm{V}\to \left(\underset{\dot{}}{[}\left(y\cap x\right)/x\underset{\dot{}}{]}x=A\leftrightarrow y\cap x=A\right)$$
36	34 35	ax-mp	$$⊢\underset{\dot{}}{[}\left(y\cap x\right)/x\underset{\dot{}}{]}x=A\leftrightarrow y\cap x=A$$
37	32 36	sylibr	$$⊢\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}x=A\wedge \underset{\dot{}}{[}x/x\underset{\dot{}}{]}x=A\right)\to \underset{\dot{}}{[}\left(y\cap x\right)/x\underset{\dot{}}{]}x=A$$
38	37	a1i	$$⊢\left(\left(A\in B\wedge A\ne \varnothing \right)\wedge y\subseteq A\wedge x\subseteq A\right)\to \left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}x=A\wedge \underset{\dot{}}{[}x/x\underset{\dot{}}{]}x=A\right)\to \underset{\dot{}}{[}\left(y\cap x\right)/x\underset{\dot{}}{]}x=A\right)$$
39	5 6 10 17 28 38	isfild	$$⊢\left(A\in B\wedge A\ne \varnothing \right)\to \left\{A\right\}\in \mathrm{Fil}\left(A\right)$$