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

Proof

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