Theorem ssficl

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

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

Proof

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