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

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 ⊢ 𝐵 ≠ ∅
Assertion fint ( 𝐹 : 𝐴 ⟶ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝐹 : 𝐴 ⟶ 𝑥 )

Proof

Step Hyp Ref Expression
1 fint.1 ⊢ 𝐵 ≠ ∅
2 ssint ⊢ ( ran 𝐹 ⊆ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 ran 𝐹 ⊆ 𝑥 )
3 2 anbi2i ⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ∩ 𝐵 ) ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ran 𝐹 ⊆ 𝑥 ) )
4 r19.28zv ⊢ ( 𝐵 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐵 ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝑥 ) ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ran 𝐹 ⊆ 𝑥 ) ) )
5 1 4 ax-mp ⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝑥 ) ↔ ( 𝐹 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐵 ran 𝐹 ⊆ 𝑥 ) )
6 3 5 bitr4i ⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ∩ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝑥 ) )
7 df-f ⊢ ( 𝐹 : 𝐴 ⟶ ∩ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ∩ 𝐵 ) )
8 df-f ⊢ ( 𝐹 : 𝐴 ⟶ 𝑥 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝑥 ) )
9 8 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐵 𝐹 : 𝐴 ⟶ 𝑥 ↔ ∀ 𝑥 ∈ 𝐵 ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝑥 ) )
10 6 7 9 3bitr4i ⊢ ( 𝐹 : 𝐴 ⟶ ∩ 𝐵 ↔ ∀ 𝑥 ∈ 𝐵 𝐹 : 𝐴 ⟶ 𝑥 )