Theorem inficl

Description: A set which is closed under pairwise intersection is closed under finite intersection. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 24-Nov-2013)

	Ref	Expression
Assertion	inficl	|- ( A e. V -> ( A. x e. A A. y e. A ( x i^i y ) e. A <-> ( fi ` A ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		ssfii	|- ( A e. V -> A C_ ( fi ` A ) )
2		eqimss2	|- ( z = A -> A C_ z )
3	2	biantrurd	|- ( z = A -> ( A. x e. z A. y e. z ( x i^i y ) e. z <-> ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) ) )
4		eleq2	|- ( z = A -> ( ( x i^i y ) e. z <-> ( x i^i y ) e. A ) )
5	4	raleqbi1dv	|- ( z = A -> ( A. y e. z ( x i^i y ) e. z <-> A. y e. A ( x i^i y ) e. A ) )
6	5	raleqbi1dv	|- ( z = A -> ( A. x e. z A. y e. z ( x i^i y ) e. z <-> A. x e. A A. y e. A ( x i^i y ) e. A ) )
7	3 6	bitr3d	|- ( z = A -> ( ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) <-> A. x e. A A. y e. A ( x i^i y ) e. A ) )
8	7	elabg	|- ( A e. V -> ( A e. { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } <-> A. x e. A A. y e. A ( x i^i y ) e. A ) )
9		intss1	|- ( A e. { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } -> |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } C_ A )
10	8 9	syl6bir	|- ( A e. V -> ( A. x e. A A. y e. A ( x i^i y ) e. A -> |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } C_ A ) )
11		dffi2	|- ( A e. V -> ( fi ` A ) = |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } )
12	11	sseq1d	|- ( A e. V -> ( ( fi ` A ) C_ A <-> |^| { z | ( A C_ z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } C_ A ) )
13	10 12	sylibrd	|- ( A e. V -> ( A. x e. A A. y e. A ( x i^i y ) e. A -> ( fi ` A ) C_ A ) )
14		eqss	|- ( ( fi ` A ) = A <-> ( ( fi ` A ) C_ A /\ A C_ ( fi ` A ) ) )
15	14	simplbi2com	|- ( A C_ ( fi ` A ) -> ( ( fi ` A ) C_ A -> ( fi ` A ) = A ) )
16	1 13 15	sylsyld	|- ( A e. V -> ( A. x e. A A. y e. A ( x i^i y ) e. A -> ( fi ` A ) = A ) )
17		fiin	|- ( ( x e. ( fi ` A ) /\ y e. ( fi ` A ) ) -> ( x i^i y ) e. ( fi ` A ) )
18	17	rgen2	|- A. x e. ( fi ` A ) A. y e. ( fi ` A ) ( x i^i y ) e. ( fi ` A )
19		eleq2	|- ( ( fi ` A ) = A -> ( ( x i^i y ) e. ( fi ` A ) <-> ( x i^i y ) e. A ) )
20	19	raleqbi1dv	|- ( ( fi ` A ) = A -> ( A. y e. ( fi ` A ) ( x i^i y ) e. ( fi ` A ) <-> A. y e. A ( x i^i y ) e. A ) )
21	20	raleqbi1dv	|- ( ( fi ` A ) = A -> ( A. x e. ( fi ` A ) A. y e. ( fi ` A ) ( x i^i y ) e. ( fi ` A ) <-> A. x e. A A. y e. A ( x i^i y ) e. A ) )
22	18 21	mpbii	|- ( ( fi ` A ) = A -> A. x e. A A. y e. A ( x i^i y ) e. A )
23	16 22	impbid1	|- ( A e. V -> ( A. x e. A A. y e. A ( x i^i y ) e. A <-> ( fi ` A ) = A ) )