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

Metamath Proof Explorer

Theorem dff2

Description: Alternate definition of a mapping. (Contributed by NM, 14-Nov-2007)

Ref Expression
Assertion dff2 ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
2 fssxp ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 ⊆ ( 𝐴 × 𝐵 ) )
3 1 2 jca ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 Fn 𝐴 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) )
4 rnss ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ran 𝐹 ⊆ ran ( 𝐴 × 𝐵 ) )
5 rnxpss ⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵
6 4 5 sstrdi ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ran 𝐹 ⊆ 𝐵 )
7 6 anim2i ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) → ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
8 df-f ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
9 7 8 sylibr ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
10 3 9 impbii ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) )