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

Theorem s1co 14869
Description: Mapping of a singleton word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
Assertion
Ref Expression
s1co ((𝑆𝐴𝐹:𝐴𝐵) → (𝐹 ∘ ⟨“𝑆”⟩) = ⟨“(𝐹𝑆)”⟩)

Proof of Theorem s1co
StepHypRef Expression
1 s1val 14633 . . . . 5 (𝑆𝐴 → ⟨“𝑆”⟩ = {⟨0, 𝑆⟩})
2 0cn 11251 . . . . . 6 0 ∈ ℂ
3 xpsng 7159 . . . . . 6 ((0 ∈ ℂ ∧ 𝑆𝐴) → ({0} × {𝑆}) = {⟨0, 𝑆⟩})
42, 3mpan 690 . . . . 5 (𝑆𝐴 → ({0} × {𝑆}) = {⟨0, 𝑆⟩})
51, 4eqtr4d 2778 . . . 4 (𝑆𝐴 → ⟨“𝑆”⟩ = ({0} × {𝑆}))
65adantr 480 . . 3 ((𝑆𝐴𝐹:𝐴𝐵) → ⟨“𝑆”⟩ = ({0} × {𝑆}))
76coeq2d 5876 . 2 ((𝑆𝐴𝐹:𝐴𝐵) → (𝐹 ∘ ⟨“𝑆”⟩) = (𝐹 ∘ ({0} × {𝑆})))
8 fvex 6920 . . . . 5 (𝐹𝑆) ∈ V
9 s1val 14633 . . . . 5 ((𝐹𝑆) ∈ V → ⟨“(𝐹𝑆)”⟩ = {⟨0, (𝐹𝑆)⟩})
108, 9ax-mp 5 . . . 4 ⟨“(𝐹𝑆)”⟩ = {⟨0, (𝐹𝑆)⟩}
11 c0ex 11253 . . . . 5 0 ∈ V
1211, 8xpsn 7161 . . . 4 ({0} × {(𝐹𝑆)}) = {⟨0, (𝐹𝑆)⟩}
1310, 12eqtr4i 2766 . . 3 ⟨“(𝐹𝑆)”⟩ = ({0} × {(𝐹𝑆)})
14 ffn 6737 . . . 4 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
15 id 22 . . . 4 (𝑆𝐴𝑆𝐴)
16 fcoconst 7154 . . . 4 ((𝐹 Fn 𝐴𝑆𝐴) → (𝐹 ∘ ({0} × {𝑆})) = ({0} × {(𝐹𝑆)}))
1714, 15, 16syl2anr 597 . . 3 ((𝑆𝐴𝐹:𝐴𝐵) → (𝐹 ∘ ({0} × {𝑆})) = ({0} × {(𝐹𝑆)}))
1813, 17eqtr4id 2794 . 2 ((𝑆𝐴𝐹:𝐴𝐵) → ⟨“(𝐹𝑆)”⟩ = (𝐹 ∘ ({0} × {𝑆})))
197, 18eqtr4d 2778 1 ((𝑆𝐴𝐹:𝐴𝐵) → (𝐹 ∘ ⟨“𝑆”⟩) = ⟨“(𝐹𝑆)”⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2106  Vcvv 3478  {csn 4631  cop 4637   × cxp 5687  ccom 5693   Fn wfn 6558  wf 6559  cfv 6563  cc 11151  0cc0 11153  ⟨“cs1 14630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-mulcl 11215  ax-i2m1 11221
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-s1 14631
This theorem is referenced by:  cats1co  14892  s2co  14956  frmdgsum  18888  frmdup2  18891  efginvrel2  19760  vrgpinv  19802  frgpup2  19809  ccatws1f1olast  32922  mrsubcv  35495
  Copyright terms: Public domain W3C validator