Metamath Proof Explorer

Theorem elfir

Description: Sufficient condition for an element of ( fiB ) . (Contributed by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion elfir ⊢ B ∈ V ∧ A ⊆ B ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ A ∈ fi ⁡ B

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ⊆ B ∧ A ≠ ∅ ∧ A ∈ Fin → A ⊆ B
2 elpw2g ⊢ B ∈ V → A ∈ 𝒫 B ↔ A ⊆ B
3 1 2 imbitrrid ⊢ B ∈ V → A ⊆ B ∧ A ≠ ∅ ∧ A ∈ Fin → A ∈ 𝒫 B
4 3 imp ⊢ B ∈ V ∧ A ⊆ B ∧ A ≠ ∅ ∧ A ∈ Fin → A ∈ 𝒫 B
5 simpr3 ⊢ B ∈ V ∧ A ⊆ B ∧ A ≠ ∅ ∧ A ∈ Fin → A ∈ Fin
6 4 5 elind ⊢ B ∈ V ∧ A ⊆ B ∧ A ≠ ∅ ∧ A ∈ Fin → A ∈ 𝒫 B ∩ Fin
7 eqid ⊢ ⋂ A = ⋂ A
8 inteq ⊢ x = A → ⋂ x = ⋂ A
9 8 rspceeqv ⊢ A ∈ 𝒫 B ∩ Fin ∧ ⋂ A = ⋂ A → ∃ x ∈ 𝒫 B ∩ Fin ⋂ A = ⋂ x
10 6 7 9 sylancl ⊢ B ∈ V ∧ A ⊆ B ∧ A ≠ ∅ ∧ A ∈ Fin → ∃ x ∈ 𝒫 B ∩ Fin ⋂ A = ⋂ x
11 simp2 ⊢ A ⊆ B ∧ A ≠ ∅ ∧ A ∈ Fin → A ≠ ∅
12 intex ⊢ A ≠ ∅ ↔ ⋂ A ∈ V
13 11 12 sylib ⊢ A ⊆ B ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ A ∈ V
14 id ⊢ B ∈ V → B ∈ V
15 elfi ⊢ ⋂ A ∈ V ∧ B ∈ V → ⋂ A ∈ fi ⁡ B ↔ ∃ x ∈ 𝒫 B ∩ Fin ⋂ A = ⋂ x
16 13 14 15 syl2anr ⊢ B ∈ V ∧ A ⊆ B ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ A ∈ fi ⁡ B ↔ ∃ x ∈ 𝒫 B ∩ Fin ⋂ A = ⋂ x
17 10 16 mpbird ⊢ B ∈ V ∧ A ⊆ B ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ A ∈ fi ⁡ B