Theorem inelfi

Description: The intersection of two sets is a finite intersection. (Contributed by Thierry Arnoux, 6-Jan-2017)

	Ref	Expression
Assertion	inelfi	|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( A i^i B ) e. ( fi ` X ) )

Proof

Step	Hyp	Ref	Expression
1		prelpwi	|- ( ( A e. X /\ B e. X ) -> { A , B } e. ~P X )
2	1	3adant1	|- ( ( X e. V /\ A e. X /\ B e. X ) -> { A , B } e. ~P X )
3		prfi	|- { A , B } e. Fin
4	3	a1i	|- ( ( X e. V /\ A e. X /\ B e. X ) -> { A , B } e. Fin )
5	2 4	elind	|- ( ( X e. V /\ A e. X /\ B e. X ) -> { A , B } e. ( ~P X i^i Fin ) )
6		intprg	|- ( ( A e. X /\ B e. X ) -> |^| { A , B } = ( A i^i B ) )
7	6	3adant1	|- ( ( X e. V /\ A e. X /\ B e. X ) -> |^| { A , B } = ( A i^i B ) )
8	7	eqcomd	|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( A i^i B ) = |^| { A , B } )
9		inteq	|- ( p = { A , B } -> |^| p = |^| { A , B } )
10	9	rspceeqv	|- ( ( { A , B } e. ( ~P X i^i Fin ) /\ ( A i^i B ) = |^| { A , B } ) -> E. p e. ( ~P X i^i Fin ) ( A i^i B ) = |^| p )
11	5 8 10	syl2anc	|- ( ( X e. V /\ A e. X /\ B e. X ) -> E. p e. ( ~P X i^i Fin ) ( A i^i B ) = |^| p )
12		inex1g	|- ( A e. X -> ( A i^i B ) e. _V )
13	12	3ad2ant2	|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( A i^i B ) e. _V )
14		simp1	|- ( ( X e. V /\ A e. X /\ B e. X ) -> X e. V )
15		elfi	|- ( ( ( A i^i B ) e. _V /\ X e. V ) -> ( ( A i^i B ) e. ( fi ` X ) <-> E. p e. ( ~P X i^i Fin ) ( A i^i B ) = |^| p ) )
16	13 14 15	syl2anc	|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( ( A i^i B ) e. ( fi ` X ) <-> E. p e. ( ~P X i^i Fin ) ( A i^i B ) = |^| p ) )
17	11 16	mpbird	|- ( ( X e. V /\ A e. X /\ B e. X ) -> ( A i^i B ) e. ( fi ` X ) )