Metamath Proof Explorer

Theorem fint

Description: Function into an intersection. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Hypothesis fint.1 ⊢ B ≠ ∅
Assertion fint ⊢ F : A ⟶ ⋂ B ↔ ∀ x ∈ B F : A ⟶ x

Proof

Step Hyp Ref Expression
1 fint.1 ⊢ B ≠ ∅
2 ssint ⊢ ran ⁡ F ⊆ ⋂ B ↔ ∀ x ∈ B ran ⁡ F ⊆ x
3 2 anbi2i ⊢ F Fn A ∧ ran ⁡ F ⊆ ⋂ B ↔ F Fn A ∧ ∀ x ∈ B ran ⁡ F ⊆ x
4 r19.28zv ⊢ B ≠ ∅ → ∀ x ∈ B F Fn A ∧ ran ⁡ F ⊆ x ↔ F Fn A ∧ ∀ x ∈ B ran ⁡ F ⊆ x
5 1 4 ax-mp ⊢ ∀ x ∈ B F Fn A ∧ ran ⁡ F ⊆ x ↔ F Fn A ∧ ∀ x ∈ B ran ⁡ F ⊆ x
6 3 5 bitr4i ⊢ F Fn A ∧ ran ⁡ F ⊆ ⋂ B ↔ ∀ x ∈ B F Fn A ∧ ran ⁡ F ⊆ x
7 df-f ⊢ F : A ⟶ ⋂ B ↔ F Fn A ∧ ran ⁡ F ⊆ ⋂ B
8 df-f ⊢ F : A ⟶ x ↔ F Fn A ∧ ran ⁡ F ⊆ x
9 8 ralbii ⊢ ∀ x ∈ B F : A ⟶ x ↔ ∀ x ∈ B F Fn A ∧ ran ⁡ F ⊆ x
10 6 7 9 3bitr4i ⊢ F : A ⟶ ⋂ B ↔ ∀ x ∈ B F : A ⟶ x