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

Metamath Proof Explorer

Theorem funssxp

Description: Two ways of specifying a partial function from A to B . (Contributed by NM, 13-Nov-2007)

Ref Expression
Assertion funssxp ( ( Fun 𝐹 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ dom 𝐹 ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
2 1 biimpi ⊢ ( Fun 𝐹 → 𝐹 Fn dom 𝐹 )
3 rnss ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ran 𝐹 ⊆ ran ( 𝐴 × 𝐵 ) )
4 rnxpss ⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵
5 3 4 sstrdi ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → ran 𝐹 ⊆ 𝐵 )
6 2 5 anim12i ⊢ ( ( Fun 𝐹 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) → ( 𝐹 Fn dom 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) )
7 df-f ⊢ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ↔ ( 𝐹 Fn dom 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) )
8 6 7 sylibr ⊢ ( ( Fun 𝐹 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) → 𝐹 : dom 𝐹 ⟶ 𝐵 )
9 dmss ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → dom 𝐹 ⊆ dom ( 𝐴 × 𝐵 ) )
10 dmxpss ⊢ dom ( 𝐴 × 𝐵 ) ⊆ 𝐴
11 9 10 sstrdi ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) → dom 𝐹 ⊆ 𝐴 )
12 11 adantl ⊢ ( ( Fun 𝐹 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) → dom 𝐹 ⊆ 𝐴 )
13 8 12 jca ⊢ ( ( Fun 𝐹 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) → ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ dom 𝐹 ⊆ 𝐴 ) )
14 ffun ⊢ ( 𝐹 : dom 𝐹 ⟶ 𝐵 → Fun 𝐹 )
15 14 adantr ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ dom 𝐹 ⊆ 𝐴 ) → Fun 𝐹 )
16 fssxp ⊢ ( 𝐹 : dom 𝐹 ⟶ 𝐵 → 𝐹 ⊆ ( dom 𝐹 × 𝐵 ) )
17 xpss1 ⊢ ( dom 𝐹 ⊆ 𝐴 → ( dom 𝐹 × 𝐵 ) ⊆ ( 𝐴 × 𝐵 ) )
18 16 17 sylan9ss ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ dom 𝐹 ⊆ 𝐴 ) → 𝐹 ⊆ ( 𝐴 × 𝐵 ) )
19 15 18 jca ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ dom 𝐹 ⊆ 𝐴 ) → ( Fun 𝐹 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) )
20 13 19 impbii ⊢ ( ( Fun 𝐹 ∧ 𝐹 ⊆ ( 𝐴 × 𝐵 ) ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐵 ∧ dom 𝐹 ⊆ 𝐴 ) )