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 = { z | z C_ B }
Assertion	ssficl	|- A. x e. A A. y e. A ( x i^i y ) e. A

Proof

Step	Hyp	Ref	Expression
1		ssficl.a	|- A = { z | z C_ B }
2		vex	|- x e. _V
3	2	inex1	|- ( x i^i y ) e. _V
4		sseq1	|- ( z = ( x i^i y ) -> ( z C_ B <-> ( x i^i y ) C_ B ) )
5		sseq1	|- ( z = x -> ( z C_ B <-> x C_ B ) )
6		sseq1	|- ( z = y -> ( z C_ B <-> y C_ B ) )
7		ssinss1	|- ( x C_ B -> ( x i^i y ) C_ B )
8	7	adantr	|- ( ( x C_ B /\ y C_ B ) -> ( x i^i y ) C_ B )
9	1 3 4 5 6 8	cllem0	|- A. x e. A A. y e. A ( x i^i y ) e. A