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

Theorem coapm 17965
Description: Composition of arrows is a partial binary operation on arrows. (Contributed by Mario Carneiro, 11-Jan-2017.)
Hypotheses
Ref Expression
coapm.o Β· = (compaβ€˜πΆ)
coapm.a 𝐴 = (Arrowβ€˜πΆ)
Assertion
Ref Expression
coapm Β· ∈ (𝐴 ↑pm (𝐴 Γ— 𝐴))

Proof of Theorem coapm
Dummy variables 𝑓 𝑔 β„Ž 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 coapm.o . . . . . 6 Β· = (compaβ€˜πΆ)
2 coapm.a . . . . . 6 𝐴 = (Arrowβ€˜πΆ)
3 eqid 2733 . . . . . 6 (compβ€˜πΆ) = (compβ€˜πΆ)
41, 2, 3coafval 17958 . . . . 5 Β· = (𝑔 ∈ 𝐴, 𝑓 ∈ {β„Ž ∈ 𝐴 ∣ (codaβ€˜β„Ž) = (domaβ€˜π‘”)} ↦ ⟨(domaβ€˜π‘“), (codaβ€˜π‘”), ((2nd β€˜π‘”)(⟨(domaβ€˜π‘“), (domaβ€˜π‘”)⟩(compβ€˜πΆ)(codaβ€˜π‘”))(2nd β€˜π‘“))⟩)
54mpofun 7484 . . . 4 Fun Β·
6 funfn 6535 . . . 4 (Fun Β· ↔ Β· Fn dom Β· )
75, 6mpbi 229 . . 3 Β· Fn dom Β·
81, 2dmcoass 17960 . . . . . . . . 9 dom Β· βŠ† (𝐴 Γ— 𝐴)
98sseli 3944 . . . . . . . 8 (𝑧 ∈ dom Β· β†’ 𝑧 ∈ (𝐴 Γ— 𝐴))
10 1st2nd2 7964 . . . . . . . 8 (𝑧 ∈ (𝐴 Γ— 𝐴) β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
119, 10syl 17 . . . . . . 7 (𝑧 ∈ dom Β· β†’ 𝑧 = ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
1211fveq2d 6850 . . . . . 6 (𝑧 ∈ dom Β· β†’ ( Β· β€˜π‘§) = ( Β· β€˜βŸ¨(1st β€˜π‘§), (2nd β€˜π‘§)⟩))
13 df-ov 7364 . . . . . 6 ((1st β€˜π‘§) Β· (2nd β€˜π‘§)) = ( Β· β€˜βŸ¨(1st β€˜π‘§), (2nd β€˜π‘§)⟩)
1412, 13eqtr4di 2791 . . . . 5 (𝑧 ∈ dom Β· β†’ ( Β· β€˜π‘§) = ((1st β€˜π‘§) Β· (2nd β€˜π‘§)))
15 eqid 2733 . . . . . . 7 (Homaβ€˜πΆ) = (Homaβ€˜πΆ)
162, 15homarw 17940 . . . . . 6 ((domaβ€˜(2nd β€˜π‘§))(Homaβ€˜πΆ)(codaβ€˜(1st β€˜π‘§))) βŠ† 𝐴
17 id 22 . . . . . . . . . . . . 13 (𝑧 ∈ dom Β· β†’ 𝑧 ∈ dom Β· )
1811, 17eqeltrrd 2835 . . . . . . . . . . . 12 (𝑧 ∈ dom Β· β†’ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ dom Β· )
19 df-br 5110 . . . . . . . . . . . 12 ((1st β€˜π‘§)dom Β· (2nd β€˜π‘§) ↔ ⟨(1st β€˜π‘§), (2nd β€˜π‘§)⟩ ∈ dom Β· )
2018, 19sylibr 233 . . . . . . . . . . 11 (𝑧 ∈ dom Β· β†’ (1st β€˜π‘§)dom Β· (2nd β€˜π‘§))
211, 2eldmcoa 17959 . . . . . . . . . . 11 ((1st β€˜π‘§)dom Β· (2nd β€˜π‘§) ↔ ((2nd β€˜π‘§) ∈ 𝐴 ∧ (1st β€˜π‘§) ∈ 𝐴 ∧ (codaβ€˜(2nd β€˜π‘§)) = (domaβ€˜(1st β€˜π‘§))))
2220, 21sylib 217 . . . . . . . . . 10 (𝑧 ∈ dom Β· β†’ ((2nd β€˜π‘§) ∈ 𝐴 ∧ (1st β€˜π‘§) ∈ 𝐴 ∧ (codaβ€˜(2nd β€˜π‘§)) = (domaβ€˜(1st β€˜π‘§))))
2322simp1d 1143 . . . . . . . . 9 (𝑧 ∈ dom Β· β†’ (2nd β€˜π‘§) ∈ 𝐴)
242, 15arwhoma 17939 . . . . . . . . 9 ((2nd β€˜π‘§) ∈ 𝐴 β†’ (2nd β€˜π‘§) ∈ ((domaβ€˜(2nd β€˜π‘§))(Homaβ€˜πΆ)(codaβ€˜(2nd β€˜π‘§))))
2523, 24syl 17 . . . . . . . 8 (𝑧 ∈ dom Β· β†’ (2nd β€˜π‘§) ∈ ((domaβ€˜(2nd β€˜π‘§))(Homaβ€˜πΆ)(codaβ€˜(2nd β€˜π‘§))))
2622simp3d 1145 . . . . . . . . 9 (𝑧 ∈ dom Β· β†’ (codaβ€˜(2nd β€˜π‘§)) = (domaβ€˜(1st β€˜π‘§)))
2726oveq2d 7377 . . . . . . . 8 (𝑧 ∈ dom Β· β†’ ((domaβ€˜(2nd β€˜π‘§))(Homaβ€˜πΆ)(codaβ€˜(2nd β€˜π‘§))) = ((domaβ€˜(2nd β€˜π‘§))(Homaβ€˜πΆ)(domaβ€˜(1st β€˜π‘§))))
2825, 27eleqtrd 2836 . . . . . . 7 (𝑧 ∈ dom Β· β†’ (2nd β€˜π‘§) ∈ ((domaβ€˜(2nd β€˜π‘§))(Homaβ€˜πΆ)(domaβ€˜(1st β€˜π‘§))))
2922simp2d 1144 . . . . . . . 8 (𝑧 ∈ dom Β· β†’ (1st β€˜π‘§) ∈ 𝐴)
302, 15arwhoma 17939 . . . . . . . 8 ((1st β€˜π‘§) ∈ 𝐴 β†’ (1st β€˜π‘§) ∈ ((domaβ€˜(1st β€˜π‘§))(Homaβ€˜πΆ)(codaβ€˜(1st β€˜π‘§))))
3129, 30syl 17 . . . . . . 7 (𝑧 ∈ dom Β· β†’ (1st β€˜π‘§) ∈ ((domaβ€˜(1st β€˜π‘§))(Homaβ€˜πΆ)(codaβ€˜(1st β€˜π‘§))))
321, 15, 28, 31coahom 17964 . . . . . 6 (𝑧 ∈ dom Β· β†’ ((1st β€˜π‘§) Β· (2nd β€˜π‘§)) ∈ ((domaβ€˜(2nd β€˜π‘§))(Homaβ€˜πΆ)(codaβ€˜(1st β€˜π‘§))))
3316, 32sselid 3946 . . . . 5 (𝑧 ∈ dom Β· β†’ ((1st β€˜π‘§) Β· (2nd β€˜π‘§)) ∈ 𝐴)
3414, 33eqeltrd 2834 . . . 4 (𝑧 ∈ dom Β· β†’ ( Β· β€˜π‘§) ∈ 𝐴)
3534rgen 3063 . . 3 βˆ€π‘§ ∈ dom Β· ( Β· β€˜π‘§) ∈ 𝐴
36 ffnfv 7070 . . 3 ( Β· :dom Β· ⟢𝐴 ↔ ( Β· Fn dom Β· ∧ βˆ€π‘§ ∈ dom Β· ( Β· β€˜π‘§) ∈ 𝐴))
377, 35, 36mpbir2an 710 . 2 Β· :dom Β· ⟢𝐴
382fvexi 6860 . . 3 𝐴 ∈ V
3938, 38xpex 7691 . . 3 (𝐴 Γ— 𝐴) ∈ V
4038, 39elpm2 8818 . 2 ( Β· ∈ (𝐴 ↑pm (𝐴 Γ— 𝐴)) ↔ ( Β· :dom Β· ⟢𝐴 ∧ dom Β· βŠ† (𝐴 Γ— 𝐴)))
4137, 8, 40mpbir2an 710 1 Β· ∈ (𝐴 ↑pm (𝐴 Γ— 𝐴))
Colors of variables: wff setvar class
Syntax hints:   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3061  {crab 3406   βŠ† wss 3914  βŸ¨cop 4596  βŸ¨cotp 4598   class class class wbr 5109   Γ— cxp 5635  dom cdm 5637  Fun wfun 6494   Fn wfn 6495  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361  1st c1st 7923  2nd c2nd 7924   ↑pm cpm 8772  compcco 17153  domacdoma 17914  codaccoda 17915  Arrowcarw 17916  Homachoma 17917  compaccoa 17948
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-ot 4599  df-uni 4870  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-id 5535  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7925  df-2nd 7926  df-pm 8774  df-cat 17556  df-doma 17918  df-coda 17919  df-homa 17920  df-arw 17921  df-coa 17950
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator