This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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