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 ⊢ C ∈ V ∧ ∀ x ∈ A B ∈ C ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ x ∈ A B ∈ fi ⁡ C

Proof

Step Hyp Ref Expression
1 simpr1 ⊢ C ∈ V ∧ ∀ x ∈ A B ∈ C ∧ A ≠ ∅ ∧ A ∈ Fin → ∀ x ∈ A B ∈ C
2 dfiin2g ⊢ ∀ x ∈ A B ∈ C → ⋂ x ∈ A B = ⋂ y | ∃ x ∈ A y = B
3 1 2 syl ⊢ C ∈ V ∧ ∀ x ∈ A B ∈ C ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ x ∈ A B = ⋂ y | ∃ x ∈ A y = B
4 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
5 4 rnmpt ⊢ ran ⁡ x ∈ A ⟼ B = y | ∃ x ∈ A y = B
6 5 inteqi ⊢ ⋂ ran ⁡ x ∈ A ⟼ B = ⋂ y | ∃ x ∈ A y = B
7 3 6 eqtr4di ⊢ C ∈ V ∧ ∀ x ∈ A B ∈ C ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ x ∈ A B = ⋂ ran ⁡ x ∈ A ⟼ B
8 4 fmpt ⊢ ∀ x ∈ A B ∈ C ↔ x ∈ A ⟼ B : A ⟶ C
9 8 3anbi1i ⊢ ∀ x ∈ A B ∈ C ∧ A ≠ ∅ ∧ A ∈ Fin ↔ x ∈ A ⟼ B : A ⟶ C ∧ A ≠ ∅ ∧ A ∈ Fin
10 intrnfi ⊢ C ∈ V ∧ x ∈ A ⟼ B : A ⟶ C ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ ran ⁡ x ∈ A ⟼ B ∈ fi ⁡ C
11 9 10 sylan2b ⊢ C ∈ V ∧ ∀ x ∈ A B ∈ C ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ ran ⁡ x ∈ A ⟼ B ∈ fi ⁡ C
12 7 11 eqeltrd ⊢ C ∈ V ∧ ∀ x ∈ A B ∈ C ∧ A ≠ ∅ ∧ A ∈ Fin → ⋂ x ∈ A B ∈ fi ⁡ C