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 → A B ∈ 𝒫 X
2 1 3adant1 ⊢ X ∈ V ∧ A ∈ X ∧ B ∈ X → A B ∈ 𝒫 X
3 prfi ⊢ A B ∈ Fin
4 3 a1i ⊢ X ∈ V ∧ A ∈ X ∧ B ∈ X → A B ∈ Fin
5 2 4 elind ⊢ X ∈ V ∧ A ∈ X ∧ B ∈ X → A B ∈ 𝒫 X ∩ Fin
6 intprg ⊢ A ∈ X ∧ B ∈ X → ⋂ A B = A ∩ B
7 6 3adant1 ⊢ X ∈ V ∧ A ∈ X ∧ B ∈ X → ⋂ A B = A ∩ B
8 7 eqcomd ⊢ X ∈ V ∧ A ∈ X ∧ B ∈ X → A ∩ B = ⋂ A B
9 inteq ⊢ p = A B → ⋂ p = ⋂ A B
10 9 rspceeqv ⊢ A B ∈ 𝒫 X ∩ Fin ∧ A ∩ B = ⋂ A B → ∃ p ∈ 𝒫 X ∩ Fin A ∩ B = ⋂ p
11 5 8 10 syl2anc ⊢ X ∈ V ∧ A ∈ X ∧ B ∈ X → ∃ p ∈ 𝒫 X ∩ Fin A ∩ 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 ∩ Fin A ∩ B = ⋂ p
16 13 14 15 syl2anc ⊢ X ∈ V ∧ A ∈ X ∧ B ∈ X → A ∩ B ∈ fi ⁡ X ↔ ∃ p ∈ 𝒫 X ∩ Fin A ∩ B = ⋂ p
17 11 16 mpbird ⊢ X ∈ V ∧ A ∈ X ∧ B ∈ X → A ∩ B ∈ fi ⁡ X