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

Metamath Proof Explorer

Theorem fin

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

Ref Expression
Assertion fin ( 𝐹 : 𝐴 ⟶ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐹 : 𝐴 ⟶ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 ssin ⊢ ( ( ran 𝐹 ⊆ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) ↔ ran 𝐹 ⊆ ( 𝐵 ∩ 𝐶 ) )
2 1 anbi2i ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( ran 𝐹 ⊆ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) ) ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ( 𝐵 ∩ 𝐶 ) ) )
3 anandi ⊢ ( ( 𝐹 Fn 𝐴 ∧ ( ran 𝐹 ⊆ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) ) ↔ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) ) )
4 2 3 bitr3i ⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ( 𝐵 ∩ 𝐶 ) ) ↔ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) ) )
5 df-f ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ ( 𝐵 ∩ 𝐶 ) ) )
6 df-f ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
7 df-f ⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) )
8 6 7 anbi12i ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐹 : 𝐴 ⟶ 𝐶 ) ↔ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ∧ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) ) )
9 4 5 8 3bitr4i ⊢ ( 𝐹 : 𝐴 ⟶ ( 𝐵 ∩ 𝐶 ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐹 : 𝐴 ⟶ 𝐶 ) )