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

Metamath Proof Explorer

Theorem iinfi

Description: An indexed intersection of elements of C is an element of the finite intersections of C . (Contributed by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion iinfi ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ ( fi ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 simpr1 ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 )
2 dfiin2g ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
3 1 2 syl ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 } )
4 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5 4 rnmpt ⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
6 5 inteqi ⊢ ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = 𝐵 }
7 3 6 eqtr4di ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 = ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
8 4 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 )
9 8 3anbi1i ⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) )
10 intrnfi ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( fi ‘ 𝐶 ) )
11 9 10 sylan2b ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ ( fi ‘ 𝐶 ) )
12 7 11 eqeltrd ⊢ ( ( 𝐶 ∈ 𝑉 ∧ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin ) ) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ ( fi ‘ 𝐶 ) )