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

Metamath Proof Explorer

Theorem elfir

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

Ref Expression
Assertion elfir ( ( 𝐵 ∈ 𝑉 ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝐴 ∈ ( fi ‘ 𝐵 ) )

Proof

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