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

Theorem arwhoma 16895
Description: An arrow is contained in the hom-set corresponding to its domain and codomain. (Contributed by Mario Carneiro, 11-Jan-2017.)
Hypotheses
Ref Expression
arwrcl.a 𝐴 = (Arrow‘𝐶)
arwhoma.h 𝐻 = (Homa𝐶)
Assertion
Ref Expression
arwhoma (𝐹𝐴𝐹 ∈ ((doma𝐹)𝐻(coda𝐹)))

Proof of Theorem arwhoma
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 arwrcl.a . . . . . . 7 𝐴 = (Arrow‘𝐶)
2 arwhoma.h . . . . . . 7 𝐻 = (Homa𝐶)
31, 2arwval 16893 . . . . . 6 𝐴 = ran 𝐻
43eleq2i 2877 . . . . 5 (𝐹𝐴𝐹 ran 𝐻)
54biimpi 207 . . . 4 (𝐹𝐴𝐹 ran 𝐻)
6 eqid 2806 . . . . . 6 (Base‘𝐶) = (Base‘𝐶)
71arwrcl 16894 . . . . . 6 (𝐹𝐴𝐶 ∈ Cat)
82, 6, 7homaf 16880 . . . . 5 (𝐹𝐴𝐻:((Base‘𝐶) × (Base‘𝐶))⟶𝒫 (((Base‘𝐶) × (Base‘𝐶)) × V))
9 ffn 6252 . . . . 5 (𝐻:((Base‘𝐶) × (Base‘𝐶))⟶𝒫 (((Base‘𝐶) × (Base‘𝐶)) × V) → 𝐻 Fn ((Base‘𝐶) × (Base‘𝐶)))
10 fnunirn 6731 . . . . 5 (𝐻 Fn ((Base‘𝐶) × (Base‘𝐶)) → (𝐹 ran 𝐻 ↔ ∃𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))𝐹 ∈ (𝐻𝑧)))
118, 9, 103syl 18 . . . 4 (𝐹𝐴 → (𝐹 ran 𝐻 ↔ ∃𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))𝐹 ∈ (𝐻𝑧)))
125, 11mpbid 223 . . 3 (𝐹𝐴 → ∃𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))𝐹 ∈ (𝐻𝑧))
13 fveq2 6404 . . . . . 6 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
14 df-ov 6873 . . . . . 6 (𝑥𝐻𝑦) = (𝐻‘⟨𝑥, 𝑦⟩)
1513, 14syl6eqr 2858 . . . . 5 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻𝑧) = (𝑥𝐻𝑦))
1615eleq2d 2871 . . . 4 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐹 ∈ (𝐻𝑧) ↔ 𝐹 ∈ (𝑥𝐻𝑦)))
1716rexxp 5466 . . 3 (∃𝑧 ∈ ((Base‘𝐶) × (Base‘𝐶))𝐹 ∈ (𝐻𝑧) ↔ ∃𝑥 ∈ (Base‘𝐶)∃𝑦 ∈ (Base‘𝐶)𝐹 ∈ (𝑥𝐻𝑦))
1812, 17sylib 209 . 2 (𝐹𝐴 → ∃𝑥 ∈ (Base‘𝐶)∃𝑦 ∈ (Base‘𝐶)𝐹 ∈ (𝑥𝐻𝑦))
19 id 22 . . . . 5 (𝐹 ∈ (𝑥𝐻𝑦) → 𝐹 ∈ (𝑥𝐻𝑦))
202homadm 16890 . . . . . 6 (𝐹 ∈ (𝑥𝐻𝑦) → (doma𝐹) = 𝑥)
212homacd 16891 . . . . . 6 (𝐹 ∈ (𝑥𝐻𝑦) → (coda𝐹) = 𝑦)
2220, 21oveq12d 6888 . . . . 5 (𝐹 ∈ (𝑥𝐻𝑦) → ((doma𝐹)𝐻(coda𝐹)) = (𝑥𝐻𝑦))
2319, 22eleqtrrd 2888 . . . 4 (𝐹 ∈ (𝑥𝐻𝑦) → 𝐹 ∈ ((doma𝐹)𝐻(coda𝐹)))
2423rexlimivw 3217 . . 3 (∃𝑦 ∈ (Base‘𝐶)𝐹 ∈ (𝑥𝐻𝑦) → 𝐹 ∈ ((doma𝐹)𝐻(coda𝐹)))
2524rexlimivw 3217 . 2 (∃𝑥 ∈ (Base‘𝐶)∃𝑦 ∈ (Base‘𝐶)𝐹 ∈ (𝑥𝐻𝑦) → 𝐹 ∈ ((doma𝐹)𝐻(coda𝐹)))
2618, 25syl 17 1 (𝐹𝐴𝐹 ∈ ((doma𝐹)𝐻(coda𝐹)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197   = wceq 1637  wcel 2156  wrex 3097  Vcvv 3391  𝒫 cpw 4351  cop 4376   cuni 4630   × cxp 5309  ran crn 5312   Fn wfn 6092  wf 6093  cfv 6097  (class class class)co 6870  Basecbs 16064  domacdoma 16870  codaccoda 16871  Arrowcarw 16872  Homachoma 16873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-ov 6873  df-1st 7394  df-2nd 7395  df-doma 16874  df-coda 16875  df-homa 16876  df-arw 16877
This theorem is referenced by:  arwdm  16897  arwcd  16898  arwhom  16901  arwdmcd  16902  coapm  16921
  Copyright terms: Public domain W3C validator