funcfn2 - Metamath Proof Explorer

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

Theorem funcfn2 18037

Description: The morphism part of a functor is a function. (Contributed by Mario Carneiro, 3-Jan-2017.)

**Hypotheses**
Ref	Expression
funcfn2.b	⊢ 𝐵 = (Base‘𝐷)
funcfn2.f	⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)

**Assertion**
Ref	Expression
funcfn2	⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵))

Proof of Theorem funcfn2 Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		funcfn2.b	. . 3 ⊢ 𝐵 = (Base‘𝐷)
2		eqid 2761	. . 3 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
3		eqid 2761	. . 3 ⊢ (Hom ‘𝐸) = (Hom ‘𝐸)
4		funcfn2.f	. . 3 ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)
5	1, 2, 3, 4	funcixp 18035	. 2 ⊢ (𝜑 → 𝐺 ∈ X𝑥 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑥))(Hom ‘𝐸)(𝐹‘(2^nd ‘𝑥))) ↑_m ((Hom ‘𝐷)‘𝑥)))
6		ixpfn 8924	. 2 ⊢ (𝐺 ∈ X𝑥 ∈ (𝐵 × 𝐵)(((𝐹‘(1^st ‘𝑥))(Hom ‘𝐸)(𝐹‘(2^nd ‘𝑥))) ↑_m ((Hom ‘𝐷)‘𝑥)) → 𝐺 Fn (𝐵 × 𝐵))
7	5, 6	syl 18	1 ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2145 class class class wbr 5103 × cxp 5649 Fn wfn 6532 ‘cfv 6537 (class class class)co 7418 1^st c1st 7997 2^nd c2nd 7998 ↑_m cmap 8840 Xcixp 8918 Basecbs 17380 Hom chom 17432 Func cfunc 18022

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-fv 6545 df-ov 7421 df-oprab 7422 df-mpo 7423 df-map 8842 df-ixp 8919 df-func 18026

This theorem is used by: funcoppc 18043 cofuval 18050 cofulid 18058 cofurid 18059 prf1st 18371 prf2nd 18372 1st2ndprf 18373 curfuncf 18405 uncfcurf 18406 curf2ndf 18414 oppfvallem 50212 uptposlem 50274 diag1 50381 prcofdiag1 50470 prcofdiag 50471 oppfdiag1 50491 oppfdiag 50493 termcfuncval 50609

W3C validator