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

Theorem cdaf 17013
Description: The codomain function is a function from arrows to objects. (Contributed by Mario Carneiro, 11-Jan-2017.)
Hypotheses
Ref Expression
arwrcl.a 𝐴 = (Arrow‘𝐶)
arwdm.b 𝐵 = (Base‘𝐶)
Assertion
Ref Expression
cdaf (coda𝐴):𝐴𝐵

Proof of Theorem cdaf
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 fo2nd 7423 . . . . . 6 2nd :V–onto→V
2 fofn 6334 . . . . . 6 (2nd :V–onto→V → 2nd Fn V)
31, 2ax-mp 5 . . . . 5 2nd Fn V
4 fo1st 7422 . . . . . 6 1st :V–onto→V
5 fof 6332 . . . . . 6 (1st :V–onto→V → 1st :V⟶V)
64, 5ax-mp 5 . . . . 5 1st :V⟶V
7 fnfco 6285 . . . . 5 ((2nd Fn V ∧ 1st :V⟶V) → (2nd ∘ 1st ) Fn V)
83, 6, 7mp2an 684 . . . 4 (2nd ∘ 1st ) Fn V
9 df-coda 16988 . . . . 5 coda = (2nd ∘ 1st )
109fneq1i 6197 . . . 4 (coda Fn V ↔ (2nd ∘ 1st ) Fn V)
118, 10mpbir 223 . . 3 coda Fn V
12 ssv 3822 . . 3 𝐴 ⊆ V
13 fnssres 6216 . . 3 ((coda Fn V ∧ 𝐴 ⊆ V) → (coda𝐴) Fn 𝐴)
1411, 12, 13mp2an 684 . 2 (coda𝐴) Fn 𝐴
15 fvres 6431 . . . 4 (𝑥𝐴 → ((coda𝐴)‘𝑥) = (coda𝑥))
16 arwrcl.a . . . . 5 𝐴 = (Arrow‘𝐶)
17 arwdm.b . . . . 5 𝐵 = (Base‘𝐶)
1816, 17arwcd 17011 . . . 4 (𝑥𝐴 → (coda𝑥) ∈ 𝐵)
1915, 18eqeltrd 2879 . . 3 (𝑥𝐴 → ((coda𝐴)‘𝑥) ∈ 𝐵)
2019rgen 3104 . 2 𝑥𝐴 ((coda𝐴)‘𝑥) ∈ 𝐵
21 ffnfv 6615 . 2 ((coda𝐴):𝐴𝐵 ↔ ((coda𝐴) Fn 𝐴 ∧ ∀𝑥𝐴 ((coda𝐴)‘𝑥) ∈ 𝐵))
2214, 20, 21mpbir2an 703 1 (coda𝐴):𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1653  wcel 2157  wral 3090  Vcvv 3386  wss 3770  cres 5315  ccom 5317   Fn wfn 6097  wf 6098  ontowfo 6100  cfv 6102  1st c1st 7400  2nd c2nd 7401  Basecbs 16183  codaccoda 16984  Arrowcarw 16985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-rep 4965  ax-sep 4976  ax-nul 4984  ax-pow 5036  ax-pr 5098  ax-un 7184
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2592  df-eu 2610  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ne 2973  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3388  df-sbc 3635  df-csb 3730  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-pw 4352  df-sn 4370  df-pr 4372  df-op 4376  df-uni 4630  df-iun 4713  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5221  df-xp 5319  df-rel 5320  df-cnv 5321  df-co 5322  df-dm 5323  df-rn 5324  df-res 5325  df-ima 5326  df-iota 6065  df-fun 6104  df-fn 6105  df-f 6106  df-f1 6107  df-fo 6108  df-f1o 6109  df-fv 6110  df-ov 6882  df-1st 7402  df-2nd 7403  df-doma 16987  df-coda 16988  df-homa 16989  df-arw 16990
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator