Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fresin Structured version   Visualization version   GIF version

Theorem fresin 6526
 Description: An identity for the mapping relationship under restriction. (Contributed by Scott Fenton, 4-Sep-2011.) (Proof shortened by Mario Carneiro, 26-May-2016.)
Assertion
Ref Expression
fresin (𝐹:𝐴𝐵 → (𝐹𝑋):(𝐴𝑋)⟶𝐵)

Proof of Theorem fresin
StepHypRef Expression
1 inss1 4157 . . 3 (𝐴𝑋) ⊆ 𝐴
2 fssres 6523 . . 3 ((𝐹:𝐴𝐵 ∧ (𝐴𝑋) ⊆ 𝐴) → (𝐹 ↾ (𝐴𝑋)):(𝐴𝑋)⟶𝐵)
31, 2mpan2 690 . 2 (𝐹:𝐴𝐵 → (𝐹 ↾ (𝐴𝑋)):(𝐴𝑋)⟶𝐵)
4 resres 5834 . . . 4 ((𝐹𝐴) ↾ 𝑋) = (𝐹 ↾ (𝐴𝑋))
5 ffn 6492 . . . . . 6 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
6 fnresdm 6443 . . . . . 6 (𝐹 Fn 𝐴 → (𝐹𝐴) = 𝐹)
75, 6syl 17 . . . . 5 (𝐹:𝐴𝐵 → (𝐹𝐴) = 𝐹)
87reseq1d 5820 . . . 4 (𝐹:𝐴𝐵 → ((𝐹𝐴) ↾ 𝑋) = (𝐹𝑋))
94, 8syl5eqr 2847 . . 3 (𝐹:𝐴𝐵 → (𝐹 ↾ (𝐴𝑋)) = (𝐹𝑋))
109feq1d 6477 . 2 (𝐹:𝐴𝐵 → ((𝐹 ↾ (𝐴𝑋)):(𝐴𝑋)⟶𝐵 ↔ (𝐹𝑋):(𝐴𝑋)⟶𝐵))
113, 10mpbid 235 1 (𝐹:𝐴𝐵 → (𝐹𝑋):(𝐴𝑋)⟶𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∩ cin 3881   ⊆ wss 3882   ↾ cres 5524   Fn wfn 6324  ⟶wf 6325 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3885  df-un 3887  df-in 3889  df-ss 3899  df-nul 4246  df-if 4428  df-sn 4528  df-pr 4530  df-op 4534  df-br 5034  df-opab 5096  df-xp 5528  df-rel 5529  df-cnv 5530  df-co 5531  df-dm 5532  df-rn 5533  df-res 5534  df-fun 6331  df-fn 6332  df-f 6333 This theorem is referenced by:  o1res  14926  limcresi  24526  dvreslem  24550  dvres2lem  24551  noreson  33343  mbfresfi  35170  limcresiooub  42368  limcresioolb  42369  limcleqr  42370  limclner  42377  mbfres2cn  42684  fouriersw  42957  sge0less  43115  sge0ssre  43120  smfres  43506
 Copyright terms: Public domain W3C validator