Theorem fss 2759

Description: Expanding the co-domain of a mapping.

Assertion

Ref	Expression
fss	⊢ ((F:A–→B ∧ B ⊆ C) → F:A–→C)

Proof of Theorem fss

Step	Hyp	Ref	Expression
1		ffn 2752	. . . 4 ⊢ (F:A–→B → F Fn A)
2	1	adantr 306	. . 3 ⊢ ((F:A–→B ∧ B ⊆ C) → F Fn A)
3		frn 2757	. . . . 5 ⊢ (F:A–→B → ran F ⊆ B)
4		sstr2 1510	. . . . 5 ⊢ (ran F ⊆ B → (B ⊆ C → ran F ⊆ C))
5	3, 4	syl 12	. . . 4 ⊢ (F:A–→B → (B ⊆ C → ran F ⊆ C))
6	5	imp 277	. . 3 ⊢ ((F:A–→B ∧ B ⊆ C) → ran F ⊆ C)
7	2, 6	jca 236	. 2 ⊢ ((F:A–→B ∧ B ⊆ C) → (F Fn A ∧ ran F ⊆ C))
8		df-f 2434	. 2 ⊢ (F:A–→C ↔ (F Fn A ∧ ran F ⊆ C))
9	7, 8	sylibr 175	1 ⊢ ((F:A–→B ∧ B ⊆ C) → F:A–→C)

Syntax hints:   → wi 2   ∧ wa 196   ⊆ wss 1487  ran crn 2411   Fn wfn 2417  –→wf 2418

This theorem is referenced by:  ffoss 2820  fsn2 2896  map0 3268  mapsn 3269  mapss 3270  ssdomg 3311  ac6lem 3575  ac6s 3577  clim0 4882  ruclem39 4923  infmap2lem2 4952  hlim0 5140  projlem26 5218  projlem29 5221  osumlem4 5533

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492  df-f 2434

metamath.org