diag11 - Metamath Proof Explorer

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

Theorem diag11 18157

Description: Value of the constant functor at an object. (Contributed by Mario Carneiro, 7-Jan-2017.) (Revised by Mario Carneiro, 15-Jan-2017.)

**Hypotheses**
Ref	Expression
diagval.l	⊢ 𝐿 = (𝐶Δ_func𝐷)
diagval.c	⊢ (𝜑 → 𝐶 ∈ Cat)
diagval.d	⊢ (𝜑 → 𝐷 ∈ Cat)
diag11.a	⊢ 𝐴 = (Base‘𝐶)
diag11.c	⊢ (𝜑 → 𝑋 ∈ 𝐴)
diag11.k	⊢ 𝐾 = ((1^st ‘𝐿)‘𝑋)
diag11.b	⊢ 𝐵 = (Base‘𝐷)
diag11.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)

**Assertion**
Ref	Expression
diag11	⊢ (𝜑 → ((1^st ‘𝐾)‘𝑌) = 𝑋)

**Proof of Theorem diag11**
Step	Hyp	Ref	Expression
1		diag11.k	. . . . 5 ⊢ 𝐾 = ((1^st ‘𝐿)‘𝑋)
2		diagval.l	. . . . . . . 8 ⊢ 𝐿 = (𝐶Δ_func𝐷)
3		diagval.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ Cat)
4		diagval.d	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ Cat)
5	2, 3, 4	diagval 18154	. . . . . . 7 ⊢ (𝜑 → 𝐿 = (⟨𝐶, 𝐷⟩ curry_F (𝐶 1^st_F 𝐷)))
6	5	fveq2d 6835	. . . . . 6 ⊢ (𝜑 → (1^st ‘𝐿) = (1^st ‘(⟨𝐶, 𝐷⟩ curry_F (𝐶 1^st_F 𝐷))))
7	6	fveq1d 6833	. . . . 5 ⊢ (𝜑 → ((1^st ‘𝐿)‘𝑋) = ((1^st ‘(⟨𝐶, 𝐷⟩ curry_F (𝐶 1^st_F 𝐷)))‘𝑋))
8	1, 7	eqtrid 2780	. . . 4 ⊢ (𝜑 → 𝐾 = ((1^st ‘(⟨𝐶, 𝐷⟩ curry_F (𝐶 1^st_F 𝐷)))‘𝑋))
9	8	fveq2d 6835	. . 3 ⊢ (𝜑 → (1^st ‘𝐾) = (1^st ‘((1^st ‘(⟨𝐶, 𝐷⟩ curry_F (𝐶 1^st_F 𝐷)))‘𝑋)))
10	9	fveq1d 6833	. 2 ⊢ (𝜑 → ((1^st ‘𝐾)‘𝑌) = ((1^st ‘((1^st ‘(⟨𝐶, 𝐷⟩ curry_F (𝐶 1^st_F 𝐷)))‘𝑋))‘𝑌))
11		eqid 2733	. . 3 ⊢ (⟨𝐶, 𝐷⟩ curry_F (𝐶 1^st_F 𝐷)) = (⟨𝐶, 𝐷⟩ curry_F (𝐶 1^st_F 𝐷))
12		diag11.a	. . 3 ⊢ 𝐴 = (Base‘𝐶)
13		eqid 2733	. . . 4 ⊢ (𝐶 ×_c 𝐷) = (𝐶 ×_c 𝐷)
14		eqid 2733	. . . 4 ⊢ (𝐶 1^st_F 𝐷) = (𝐶 1^st_F 𝐷)
15	13, 3, 4, 14	1stfcl 18111	. . 3 ⊢ (𝜑 → (𝐶 1^st_F 𝐷) ∈ ((𝐶 ×_c 𝐷) Func 𝐶))
16		diag11.b	. . 3 ⊢ 𝐵 = (Base‘𝐷)
17		diag11.c	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
18		eqid 2733	. . 3 ⊢ ((1^st ‘(⟨𝐶, 𝐷⟩ curry_F (𝐶 1^st_F 𝐷)))‘𝑋) = ((1^st ‘(⟨𝐶, 𝐷⟩ curry_F (𝐶 1^st_F 𝐷)))‘𝑋)
19		diag11.y	. . 3 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
20	11, 12, 3, 4, 15, 16, 17, 18, 19	curf11 18140	. 2 ⊢ (𝜑 → ((1^st ‘((1^st ‘(⟨𝐶, 𝐷⟩ curry_F (𝐶 1^st_F 𝐷)))‘𝑋))‘𝑌) = (𝑋(1^st ‘(𝐶 1^st_F 𝐷))𝑌))
21		df-ov 7358	. . . 4 ⊢ (𝑋(1^st ‘(𝐶 1^st_F 𝐷))𝑌) = ((1^st ‘(𝐶 1^st_F 𝐷))‘⟨𝑋, 𝑌⟩)
22	13, 12, 16	xpcbas 18092	. . . . 5 ⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×_c 𝐷))
23		eqid 2733	. . . . 5 ⊢ (Hom ‘(𝐶 ×_c 𝐷)) = (Hom ‘(𝐶 ×_c 𝐷))
24	17, 19	opelxpd 5660	. . . . 5 ⊢ (𝜑 → ⟨𝑋, 𝑌⟩ ∈ (𝐴 × 𝐵))
25	13, 22, 23, 3, 4, 14, 24	1stf1 18106	. . . 4 ⊢ (𝜑 → ((1^st ‘(𝐶 1^st_F 𝐷))‘⟨𝑋, 𝑌⟩) = (1^st ‘⟨𝑋, 𝑌⟩))
26	21, 25	eqtrid 2780	. . 3 ⊢ (𝜑 → (𝑋(1^st ‘(𝐶 1^st_F 𝐷))𝑌) = (1^st ‘⟨𝑋, 𝑌⟩))
27		op1stg 7942	. . . 4 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (1^st ‘⟨𝑋, 𝑌⟩) = 𝑋)
28	17, 19, 27	syl2anc 584	. . 3 ⊢ (𝜑 → (1^st ‘⟨𝑋, 𝑌⟩) = 𝑋)
29	26, 28	eqtrd 2768	. 2 ⊢ (𝜑 → (𝑋(1^st ‘(𝐶 1^st_F 𝐷))𝑌) = 𝑋)
30	10, 20, 29	3eqtrd 2772	1 ⊢ (𝜑 → ((1^st ‘𝐾)‘𝑌) = 𝑋)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2113 ⟨cop 4583 × cxp 5619 ‘cfv 6489 (class class class)co 7355 1^st c1st 7928 Basecbs 17127 Hom chom 17179 Catccat 17578 ×_c cxpc 18082 1^st_F c1stf 18083 curry_F ccurf 18124 Δ_funccdiag 18126

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-cnex 11073 ax-resscn 11074 ax-1cn 11075 ax-icn 11076 ax-addcl 11077 ax-addrcl 11078 ax-mulcl 11079 ax-mulrcl 11080 ax-mulcom 11081 ax-addass 11082 ax-mulass 11083 ax-distr 11084 ax-i2m1 11085 ax-1ne0 11086 ax-1rid 11087 ax-rnegex 11088 ax-rrecex 11089 ax-cnre 11090 ax-pre-lttri 11091 ax-pre-lttrn 11092 ax-pre-ltadd 11093 ax-pre-mulgt0 11094

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-tp 4582 df-op 4584 df-uni 4861 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7312 df-ov 7358 df-oprab 7359 df-mpo 7360 df-om 7806 df-1st 7930 df-2nd 7931 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-er 8631 df-map 8761 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-pnf 11159 df-mnf 11160 df-xr 11161 df-ltxr 11162 df-le 11163 df-sub 11357 df-neg 11358 df-nn 12137 df-2 12199 df-3 12200 df-4 12201 df-5 12202 df-6 12203 df-7 12204 df-8 12205 df-9 12206 df-n0 12393 df-z 12480 df-dec 12599 df-uz 12743 df-fz 13415 df-struct 17065 df-slot 17100 df-ndx 17112 df-base 17128 df-hom 17192 df-cco 17193 df-cat 17582 df-cid 17583 df-func 17773 df-xpc 18086 df-1stf 18087 df-curf 18128 df-diag 18130

This theorem is referenced by: curf2ndf 18161 diag1 49465 prcofdiag1 49554 oppfdiag1 49575 isinito2lem 49659 isinito3 49661 diag2f1olem 49697 concl 49822 coccl 49823 concom 49824 coccom 49825 islmd 49826 iscmd 49827

W3C validator