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 𝐹 ⊆ 𝐴 ) )