xpchom - Metamath Proof Explorer

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

Theorem xpchom 18361

Description: Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017.)

**Hypotheses**
Ref	Expression
xpchomfval.t	⊢ 𝑇 = (𝐶 ×_c 𝐷)
xpchomfval.y	⊢ 𝐵 = (Base‘𝑇)
xpchomfval.h	⊢ 𝐻 = (Hom ‘𝐶)
xpchomfval.j	⊢ 𝐽 = (Hom ‘𝐷)
xpchomfval.k	⊢ 𝐾 = (Hom ‘𝑇)
xpchom.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
xpchom.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)

**Assertion**
Ref	Expression
xpchom	⊢ (𝜑 → (𝑋𝐾𝑌) = (((1^st ‘𝑋)𝐻(1^st ‘𝑌)) × ((2^nd ‘𝑋)𝐽(2^nd ‘𝑌))))

Proof of Theorem xpchom Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpchom.x	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
2		xpchom.y	. 2 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
3		simpl 488	. . . . . 6 ⊢ ((𝑢 = 𝑋 ∧ 𝑣 = 𝑌) → 𝑢 = 𝑋)
4	3	fveq2d 6892	. . . . 5 ⊢ ((𝑢 = 𝑋 ∧ 𝑣 = 𝑌) → (1^st ‘𝑢) = (1^st ‘𝑋))
5		simpr 490	. . . . . 6 ⊢ ((𝑢 = 𝑋 ∧ 𝑣 = 𝑌) → 𝑣 = 𝑌)
6	5	fveq2d 6892	. . . . 5 ⊢ ((𝑢 = 𝑋 ∧ 𝑣 = 𝑌) → (1^st ‘𝑣) = (1^st ‘𝑌))
7	4, 6	oveq12d 7440	. . . 4 ⊢ ((𝑢 = 𝑋 ∧ 𝑣 = 𝑌) → ((1^st ‘𝑢)𝐻(1^st ‘𝑣)) = ((1^st ‘𝑋)𝐻(1^st ‘𝑌)))
8	3	fveq2d 6892	. . . . 5 ⊢ ((𝑢 = 𝑋 ∧ 𝑣 = 𝑌) → (2^nd ‘𝑢) = (2^nd ‘𝑋))
9	5	fveq2d 6892	. . . . 5 ⊢ ((𝑢 = 𝑋 ∧ 𝑣 = 𝑌) → (2^nd ‘𝑣) = (2^nd ‘𝑌))
10	8, 9	oveq12d 7440	. . . 4 ⊢ ((𝑢 = 𝑋 ∧ 𝑣 = 𝑌) → ((2^nd ‘𝑢)𝐽(2^nd ‘𝑣)) = ((2^nd ‘𝑋)𝐽(2^nd ‘𝑌)))
11	7, 10	xpeq12d 5681	. . 3 ⊢ ((𝑢 = 𝑋 ∧ 𝑣 = 𝑌) → (((1^st ‘𝑢)𝐻(1^st ‘𝑣)) × ((2^nd ‘𝑢)𝐽(2^nd ‘𝑣))) = (((1^st ‘𝑋)𝐻(1^st ‘𝑌)) × ((2^nd ‘𝑋)𝐽(2^nd ‘𝑌))))
12		xpchomfval.t	. . . 4 ⊢ 𝑇 = (𝐶 ×_c 𝐷)
13		xpchomfval.y	. . . 4 ⊢ 𝐵 = (Base‘𝑇)
14		xpchomfval.h	. . . 4 ⊢ 𝐻 = (Hom ‘𝐶)
15		xpchomfval.j	. . . 4 ⊢ 𝐽 = (Hom ‘𝐷)
16		xpchomfval.k	. . . 4 ⊢ 𝐾 = (Hom ‘𝑇)
17	12, 13, 14, 15, 16	xpchomfval 18360	. . 3 ⊢ 𝐾 = (𝑢 ∈ 𝐵, 𝑣 ∈ 𝐵 ↦ (((1^st ‘𝑢)𝐻(1^st ‘𝑣)) × ((2^nd ‘𝑢)𝐽(2^nd ‘𝑣))))
18		ovex 7455	. . . 4 ⊢ ((1^st ‘𝑋)𝐻(1^st ‘𝑌)) ∈ V
19		ovex 7455	. . . 4 ⊢ ((2^nd ‘𝑋)𝐽(2^nd ‘𝑌)) ∈ V
20	18, 19	xpex 7769	. . 3 ⊢ (((1^st ‘𝑋)𝐻(1^st ‘𝑌)) × ((2^nd ‘𝑋)𝐽(2^nd ‘𝑌))) ∈ V
21	11, 17, 20	ovmpoa 7577	. 2 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐾𝑌) = (((1^st ‘𝑋)𝐻(1^st ‘𝑌)) × ((2^nd ‘𝑋)𝐽(2^nd ‘𝑌))))
22	1, 2, 21	syl2anc 596	1 ⊢ (𝜑 → (𝑋𝐾𝑌) = (((1^st ‘𝑋)𝐻(1^st ‘𝑌)) × ((2^nd ‘𝑋)𝐽(2^nd ‘𝑌))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 = wceq 1569 ∈ wcel 2144 × cxp 5648 ‘cfv 6541 (class class class)co 7422 1^st c1st 8001 2^nd c2nd 8002 Basecbs 17394 Hom chom 17446 ×_c cxpc 18349

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7753 ax-cnex 11261 ax-resscn 11262 ax-1cn 11263 ax-icn 11264 ax-addcl 11265 ax-addrcl 11266 ax-mulcl 11267 ax-mulrcl 11268 ax-mulcom 11269 ax-addass 11270 ax-mulass 11271 ax-distr 11272 ax-i2m1 11273 ax-1ne0 11274 ax-1rid 11275 ax-rnegex 11276 ax-rrecex 11277 ax-cnre 11278 ax-pre-lttri 11279 ax-pre-lttrn 11280 ax-pre-ltadd 11281 ax-pre-mulgt0 11282

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7379 df-ov 7425 df-oprab 7426 df-mpo 7427 df-om 7880 df-1st 8003 df-2nd 8004 df-frecs 8304 df-wrecs 8335 df-recs 8384 df-rdg 8423 df-1o 8481 df-er 8722 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-pnf 11350 df-mnf 11351 df-xr 11352 df-ltxr 11353 df-le 11354 df-sub 11548 df-neg 11549 df-nn 12341 df-2 12410 df-3 12411 df-4 12412 df-5 12413 df-6 12414 df-7 12415 df-8 12416 df-9 12417 df-n0 12612 df-z 12699 df-dec 12820 df-uz 12971 df-fz 13645 df-struct 17332 df-slot 17367 df-ndx 17379 df-base 17395 df-hom 17459 df-cco 17460 df-xpc 18353

This theorem is used by: xpchom2 18367 xpccatid 18369 1stfcl 18378 2ndfcl 18379 xpcpropd 18389 evlfcl 18403 curf1cl 18409 hofcl 18440 yonedalem3 18461 xpcfuchom 50483 dfswapf2 50490 swapf2a 50500 swapf2f1oaALT 50507 oppc1stf 50517 oppc2ndf 50518

W3C validator