Theorem supfil

Description: The supersets of a nonempty set which are also subsets of a given base set form a filter. (Contributed by Jeff Hankins, 12-Nov-2009) (Revised by Stefan O'Rear, 7-Aug-2015)

	Ref	Expression
Assertion	supfil	$$⊢\left(A\in V\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \left\{x\in 𝒫A|B\subseteq x\right\}\in \mathrm{Fil}\left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		sseq2	$$⊢x=y\to \left(B\subseteq x\leftrightarrow B\subseteq y\right)$$
2	1	elrab	$$⊢y\in \left\{x\in 𝒫A|B\subseteq x\right\}\leftrightarrow \left(y\in 𝒫A\wedge B\subseteq y\right)$$
3		velpw	$$⊢y\in 𝒫A\leftrightarrow y\subseteq A$$
4	3	anbi1i	$$⊢\left(y\in 𝒫A\wedge B\subseteq y\right)\leftrightarrow \left(y\subseteq A\wedge B\subseteq y\right)$$
5	2 4	bitri	$$⊢y\in \left\{x\in 𝒫A|B\subseteq x\right\}\leftrightarrow \left(y\subseteq A\wedge B\subseteq y\right)$$
6	5	a1i	$$⊢\left(A\in V\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \left(y\in \left\{x\in 𝒫A|B\subseteq x\right\}\leftrightarrow \left(y\subseteq A\wedge B\subseteq y\right)\right)$$
7		simp1	$$⊢\left(A\in V\wedge B\subseteq A\wedge B\ne \varnothing \right)\to A\in V$$
8		simp2	$$⊢\left(A\in V\wedge B\subseteq A\wedge B\ne \varnothing \right)\to B\subseteq A$$
9		sseq2	$$⊢y=A\to \left(B\subseteq y\leftrightarrow B\subseteq A\right)$$
10	9	sbcieg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}B\subseteq y\leftrightarrow B\subseteq A\right)$$
11	7 10	syl	$$⊢\left(A\in V\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \left(\underset{\dot{}}{[}A/y\underset{\dot{}}{]}B\subseteq y\leftrightarrow B\subseteq A\right)$$
12	8 11	mpbird	$$⊢\left(A\in V\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \underset{\dot{}}{[}A/y\underset{\dot{}}{]}B\subseteq y$$
13		ss0	$$⊢B\subseteq \varnothing \to B=\varnothing$$
14	13	necon3ai	$$⊢B\ne \varnothing \to \neg B\subseteq \varnothing$$
15	14	3ad2ant3	$$⊢\left(A\in V\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \neg B\subseteq \varnothing$$
16		0ex	$$⊢\varnothing \in \mathrm{V}$$
17		sseq2	$$⊢y=\varnothing \to \left(B\subseteq y\leftrightarrow B\subseteq \varnothing \right)$$
18	16 17	sbcie	$$⊢\underset{\dot{}}{[}\varnothing /y\underset{\dot{}}{]}B\subseteq y\leftrightarrow B\subseteq \varnothing$$
19	15 18	sylnibr	$$⊢\left(A\in V\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \neg \underset{\dot{}}{[}\varnothing /y\underset{\dot{}}{]}B\subseteq y$$
20		sstr	$$⊢\left(B\subseteq w\wedge w\subseteq z\right)\to B\subseteq z$$
21	20	expcom	$$⊢w\subseteq z\to \left(B\subseteq w\to B\subseteq z\right)$$
22		vex	$$⊢w\in \mathrm{V}$$
23		sseq2	$$⊢y=w\to \left(B\subseteq y\leftrightarrow B\subseteq w\right)$$
24	22 23	sbcie	$$⊢\underset{\dot{}}{[}w/y\underset{\dot{}}{]}B\subseteq y\leftrightarrow B\subseteq w$$
25		vex	$$⊢z\in \mathrm{V}$$
26		sseq2	$$⊢y=z\to \left(B\subseteq y\leftrightarrow B\subseteq z\right)$$
27	25 26	sbcie	$$⊢\underset{\dot{}}{[}z/y\underset{\dot{}}{]}B\subseteq y\leftrightarrow B\subseteq z$$
28	21 24 27	3imtr4g	$$⊢w\subseteq z\to \left(\underset{\dot{}}{[}w/y\underset{\dot{}}{]}B\subseteq y\to \underset{\dot{}}{[}z/y\underset{\dot{}}{]}B\subseteq y\right)$$
29	28	3ad2ant3	$$⊢\left(\left(A\in V\wedge B\subseteq A\wedge B\ne \varnothing \right)\wedge z\subseteq A\wedge w\subseteq z\right)\to \left(\underset{\dot{}}{[}w/y\underset{\dot{}}{]}B\subseteq y\to \underset{\dot{}}{[}z/y\underset{\dot{}}{]}B\subseteq y\right)$$
30		ssin	$$⊢\left(B\subseteq z\wedge B\subseteq w\right)\leftrightarrow B\subseteq z\cap w$$
31	30	biimpi	$$⊢\left(B\subseteq z\wedge B\subseteq w\right)\to B\subseteq z\cap w$$
32	27 24 31	syl2anb	$$⊢\left(\underset{\dot{}}{[}z/y\underset{\dot{}}{]}B\subseteq y\wedge \underset{\dot{}}{[}w/y\underset{\dot{}}{]}B\subseteq y\right)\to B\subseteq z\cap w$$
33	25	inex1	$$⊢z\cap w\in \mathrm{V}$$
34		sseq2	$$⊢y=z\cap w\to \left(B\subseteq y\leftrightarrow B\subseteq z\cap w\right)$$
35	33 34	sbcie	$$⊢\underset{\dot{}}{[}\left(z\cap w\right)/y\underset{\dot{}}{]}B\subseteq y\leftrightarrow B\subseteq z\cap w$$
36	32 35	sylibr	$$⊢\left(\underset{\dot{}}{[}z/y\underset{\dot{}}{]}B\subseteq y\wedge \underset{\dot{}}{[}w/y\underset{\dot{}}{]}B\subseteq y\right)\to \underset{\dot{}}{[}\left(z\cap w\right)/y\underset{\dot{}}{]}B\subseteq y$$
37	36	a1i	$$⊢\left(\left(A\in V\wedge B\subseteq A\wedge B\ne \varnothing \right)\wedge z\subseteq A\wedge w\subseteq A\right)\to \left(\left(\underset{\dot{}}{[}z/y\underset{\dot{}}{]}B\subseteq y\wedge \underset{\dot{}}{[}w/y\underset{\dot{}}{]}B\subseteq y\right)\to \underset{\dot{}}{[}\left(z\cap w\right)/y\underset{\dot{}}{]}B\subseteq y\right)$$
38	6 7 12 19 29 37	isfild	$$⊢\left(A\in V\wedge B\subseteq A\wedge B\ne \varnothing \right)\to \left\{x\in 𝒫A|B\subseteq x\right\}\in \mathrm{Fil}\left(A\right)$$