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∈V∧A∈X∧B∈X→A∩B∈fi⁡X

Proof

Step Hyp Ref Expression
1 prelpwi ⊢A∈X∧B∈X→AB∈𝒫X
2 1 3adant1 ⊢X∈V∧A∈X∧B∈X→AB∈𝒫X
3 prfi ⊢AB∈Fin
4 3 a1i ⊢X∈V∧A∈X∧B∈X→AB∈Fin
5 2 4 elind ⊢X∈V∧A∈X∧B∈X→AB∈𝒫X∩Fin
6 intprg ⊢A∈X∧B∈X→⋂AB=A∩B
7 6 3adant1 ⊢X∈V∧A∈X∧B∈X→⋂AB=A∩B
8 7 eqcomd ⊢X∈V∧A∈X∧B∈X→A∩B=⋂AB
9 inteq ⊢p=AB→⋂p=⋂AB
10 9 rspceeqv ⊢AB∈𝒫X∩Fin∧A∩B=⋂AB→∃p∈𝒫X∩FinA∩B=⋂p
11 5 8 10 syl2anc ⊢X∈V∧A∈X∧B∈X→∃p∈𝒫X∩FinA∩B=⋂p
12 inex1g ⊢A∈X→A∩B∈V
13 12 3ad2ant2 ⊢X∈V∧A∈X∧B∈X→A∩B∈V
14 simp1 ⊢X∈V∧A∈X∧B∈X→X∈V
15 elfi ⊢A∩B∈V∧X∈V→A∩B∈fi⁡X↔∃p∈𝒫X∩FinA∩B=⋂p
16 13 14 15 syl2anc ⊢X∈V∧A∈X∧B∈X→A∩B∈fi⁡X↔∃p∈𝒫X∩FinA∩B=⋂p
17 11 16 mpbird ⊢X∈V∧A∈X∧B∈X→A∩B∈fi⁡X