Theorem superficl

Description: The class of all supersets of a class has the finite intersection property. (Contributed by RP, 1-Jan-2020) (Proof shortened by RP, 3-Jan-2020)

	Ref	Expression
Hypothesis	superficl.a	$$⊢A=\left\{z|B\subseteq z\right\}$$
Assertion	superficl	$$⊢\forall x\in A\forall y\in Ax\cap y\in A$$

Proof

Step	Hyp	Ref	Expression
1		superficl.a	$$⊢A=\left\{z|B\subseteq z\right\}$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	inex1	$$⊢x\cap y\in \mathrm{V}$$
4		sseq2	$$⊢z=x\cap y\to \left(B\subseteq z\leftrightarrow B\subseteq x\cap y\right)$$
5		sseq2	$$⊢z=x\to \left(B\subseteq z\leftrightarrow B\subseteq x\right)$$
6		sseq2	$$⊢z=y\to \left(B\subseteq z\leftrightarrow B\subseteq y\right)$$
7		ssin	$$⊢\left(B\subseteq x\wedge B\subseteq y\right)\leftrightarrow B\subseteq x\cap y$$
8	7	biimpi	$$⊢\left(B\subseteq x\wedge B\subseteq y\right)\to B\subseteq x\cap y$$
9	1 3 4 5 6 8	cllem0	$$⊢\forall x\in A\forall y\in Ax\cap y\in A$$