curf1fval - Metamath Proof Explorer

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

Theorem curf1fval 18213

Description: Value of the object part of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.)

**Hypotheses**
Ref	Expression
curfval.g	⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curry_F 𝐹)
curfval.a	⊢ 𝐴 = (Base‘𝐶)
curfval.c	⊢ (𝜑 → 𝐶 ∈ Cat)
curfval.d	⊢ (𝜑 → 𝐷 ∈ Cat)
curfval.f	⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×_c 𝐷) Func 𝐸))
curfval.b	⊢ 𝐵 = (Base‘𝐷)
curfval.j	⊢ 𝐽 = (Hom ‘𝐷)
curfval.1	⊢ 1 = (Id‘𝐶)

**Assertion**
Ref	Expression
curf1fval	⊢ (𝜑 → (1^st ‘𝐺) = (𝑥 ∈ 𝐴 ↦ ⟨(𝑦 ∈ 𝐵 ↦ (𝑥(1^st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(⟨𝑥, 𝑦⟩(2^nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩))

Distinct variable groups: 𝑥,𝑔,𝑦,𝑧, 1 𝑥,𝐴,𝑦 𝐵,𝑔,𝑥,𝑦,𝑧 𝐶,𝑔,𝑥,𝑦,𝑧 𝐷,𝑔,𝑥,𝑦,𝑧 𝜑,𝑔,𝑥,𝑦,𝑧 𝑔,𝐸,𝑦,𝑧 𝑔,𝐽,𝑥 𝑔,𝐹,𝑥,𝑦,𝑧 Allowed substitution hints: 𝐴(𝑧,𝑔) 𝐸(𝑥) 𝐺(𝑥,𝑦,𝑧,𝑔) 𝐽(𝑦,𝑧)

**Proof of Theorem curf1fval**
Step	Hyp	Ref	Expression
1		curfval.g	. . 3 ⊢ 𝐺 = (⟨𝐶, 𝐷⟩ curry_F 𝐹)
2		curfval.a	. . 3 ⊢ 𝐴 = (Base‘𝐶)
3		curfval.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ Cat)
4		curfval.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ Cat)
5		curfval.f	. . 3 ⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×_c 𝐷) Func 𝐸))
6		curfval.b	. . 3 ⊢ 𝐵 = (Base‘𝐷)
7		curfval.j	. . 3 ⊢ 𝐽 = (Hom ‘𝐷)
8		curfval.1	. . 3 ⊢ 1 = (Id‘𝐶)
9		eqid 2725	. . 3 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
10		eqid 2725	. . 3 ⊢ (Id‘𝐷) = (Id‘𝐷)
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	curfval 18212	. 2 ⊢ (𝜑 → 𝐺 = ⟨(𝑥 ∈ 𝐴 ↦ ⟨(𝑦 ∈ 𝐵 ↦ (𝑥(1^st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(⟨𝑥, 𝑦⟩(2^nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2^nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))⟩)
12	2	fvexi 6905	. . . 4 ⊢ 𝐴 ∈ V
13	12	mptex 7230	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ ⟨(𝑦 ∈ 𝐵 ↦ (𝑥(1^st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(⟨𝑥, 𝑦⟩(2^nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩) ∈ V
14	12, 12	mpoex 8080	. . 3 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2^nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧))))) ∈ V
15	13, 14	op1std 7999	. 2 ⊢ (𝐺 = ⟨(𝑥 ∈ 𝐴 ↦ ⟨(𝑦 ∈ 𝐵 ↦ (𝑥(1^st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(⟨𝑥, 𝑦⟩(2^nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ (𝑔 ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ (𝑧 ∈ 𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2^nd ‘𝐹)⟨𝑦, 𝑧⟩)((Id‘𝐷)‘𝑧)))))⟩ → (1^st ‘𝐺) = (𝑥 ∈ 𝐴 ↦ ⟨(𝑦 ∈ 𝐵 ↦ (𝑥(1^st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(⟨𝑥, 𝑦⟩(2^nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩))
16	11, 15	syl 17	1 ⊢ (𝜑 → (1^st ‘𝐺) = (𝑥 ∈ 𝐴 ↦ ⟨(𝑦 ∈ 𝐵 ↦ (𝑥(1^st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1 ‘𝑥)(⟨𝑥, 𝑦⟩(2^nd ‘𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 ⟨cop 4630 ↦ cmpt 5226 ‘cfv 6542 (class class class)co 7415 ∈ cmpo 7417 1^st c1st 7987 2^nd c2nd 7988 Basecbs 17177 Hom chom 17241 Catccat 17641 Idccid 17642 Func cfunc 17837 ×_c cxpc 18156 curry_F ccurf 18199

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5280 ax-sep 5294 ax-nul 5301 ax-pow 5359 ax-pr 5423 ax-un 7737

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3770 df-csb 3886 df-dif 3943 df-un 3945 df-in 3947 df-ss 3957 df-nul 4319 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5227 df-id 5570 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-res 5684 df-ima 5685 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-ov 7418 df-oprab 7419 df-mpo 7420 df-1st 7989 df-2nd 7990 df-curf 18203

This theorem is referenced by: curf1 18214

W3C validator

	
		OSZAR »