Metamath Proof Explorer


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 ) )