Theorem cncfss 23590

Description: The set of continuous functions is expanded when the range is expanded. (Contributed by Mario Carneiro, 30-Aug-2014.)

Assertion

Ref	Expression
cncfss	⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) → (𝐴–cn→𝐵) ⊆ (𝐴–cn→𝐶))

Proof of Theorem cncfss

Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cncff 23584	. . . . . 6 ⊢ (𝑓 ∈ (𝐴–cn→𝐵) → 𝑓:𝐴⟶𝐵)
2	1	adantl 486	. . . . 5 ⊢ (((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) ∧ 𝑓 ∈ (𝐴–cn→𝐵)) → 𝑓:𝐴⟶𝐵)
3		simpll 767	. . . . 5 ⊢ (((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) ∧ 𝑓 ∈ (𝐴–cn→𝐵)) → 𝐵 ⊆ 𝐶)
4	2, 3	fssd 6511	. . . 4 ⊢ (((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) ∧ 𝑓 ∈ (𝐴–cn→𝐵)) → 𝑓:𝐴⟶𝐶)
5		cncffvrn 23589	. . . . 5 ⊢ ((𝐶 ⊆ ℂ ∧ 𝑓 ∈ (𝐴–cn→𝐵)) → (𝑓 ∈ (𝐴–cn→𝐶) ↔ 𝑓:𝐴⟶𝐶))
6	5	adantll 714	. . . 4 ⊢ (((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) ∧ 𝑓 ∈ (𝐴–cn→𝐵)) → (𝑓 ∈ (𝐴–cn→𝐶) ↔ 𝑓:𝐴⟶𝐶))
7	4, 6	mpbird 260	. . 3 ⊢ (((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) ∧ 𝑓 ∈ (𝐴–cn→𝐵)) → 𝑓 ∈ (𝐴–cn→𝐶))
8	7	ex 417	. 2 ⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) → (𝑓 ∈ (𝐴–cn→𝐵) → 𝑓 ∈ (𝐴–cn→𝐶)))
9	8	ssrdv 3899	1 ⊢ ((𝐵 ⊆ 𝐶 ∧ 𝐶 ⊆ ℂ) → (𝐴–cn→𝐵) ⊆ (𝐴–cn→𝐶))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∈ wcel 2112   ⊆ wss 3859  ⟶wf 6329  (class class class)co 7148  ℂcc 10563  –cn→ccncf 23567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7457  ax-cnex 10621  ax-resscn 10622  ax-1cn 10623  ax-icn 10624  ax-addcl 10625  ax-addrcl 10626  ax-mulcl 10627  ax-mulrcl 10628  ax-mulcom 10629  ax-addass 10630  ax-mulass 10631  ax-distr 10632  ax-i2m1 10633  ax-1ne0 10634  ax-1rid 10635  ax-rnegex 10636  ax-rrecex 10637  ax-cnre 10638  ax-pre-lttri 10639  ax-pre-lttrn 10640  ax-pre-ltadd 10641  ax-pre-mulgt0 10642

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-nul 4227  df-if 4419  df-pw 4494  df-sn 4521  df-pr 4523  df-op 4527  df-uni 4797  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5428  df-po 5441  df-so 5442  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-ima 5535  df-iota 6292  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-er 8297  df-map 8416  df-en 8526  df-dom 8527  df-sdom 8528  df-pnf 10705  df-mnf 10706  df-xr 10707  df-ltxr 10708  df-le 10709  df-sub 10900  df-neg 10901  df-div 11326  df-2 11727  df-cj 14496  df-re 14497  df-im 14498  df-abs 14633  df-cncf 23569

This theorem is referenced by:  cncfcompt2  23599  cncfmptid  23604  cncfmpt2ss  23607  evthicc2  24150  volivth  24297  iblabslem  24517  iblabs  24518  bddmulibl  24528  cnlimci  24578  rolle  24679  c1liplem1  24685  dvivth  24699  dvcnvrelem2  24707  itgsubst  24738  logcn  25327  logccv  25343  fdvposlt  32088  fdvneggt  32089  fdvposle  32090  fdvnegge  32091  logdivsqrle  32139  knoppcnlem10  34221  ftc1cnnclem  35398  ftc2nc  35409  areacirclem2  35416  evthiccabs  42489  cncfcompt  42881  cncficcgt0  42886  cncfiooicc  42892  cncfiooiccre  42893  itgsubsticclem  42973  fourierdlem72  43176  fourierdlem78  43182  fourierdlem83  43187  fourierdlem84  43188  fourierdlem85  43189  fourierdlem88  43192  fourierdlem95  43199  fourierdlem111  43215