Theorem isfuncd 17954

Description: Deduce that an operation is a functor of categories. (Contributed by Mario Carneiro, 4-Jan-2017.)

Hypotheses

Ref	Expression
isfunc.b	⊢ 𝐵 = (Base‘𝐷)
isfunc.c	⊢ 𝐶 = (Base‘𝐸)
isfunc.h	⊢ 𝐻 = (Hom ‘𝐷)
isfunc.j	⊢ 𝐽 = (Hom ‘𝐸)
isfunc.1	⊢ 1 = (Id‘𝐷)
isfunc.i	⊢ 𝐼 = (Id‘𝐸)
isfunc.x	⊢ · = (comp‘𝐷)
isfunc.o	⊢ 𝑂 = (comp‘𝐸)
isfunc.d	⊢ (𝜑 → 𝐷 ∈ Cat)
isfunc.e	⊢ (𝜑 → 𝐸 ∈ Cat)
isfuncd.1	⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
isfuncd.2	⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵))
isfuncd.3	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦)))
isfuncd.4	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
isfuncd.5	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧))) → ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))

Assertion

Ref	Expression
isfuncd	⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)

Distinct variable groups:   𝑚,𝑛,𝑥,𝑦,𝑧,𝐵   𝐷,𝑚,𝑛,𝑥,𝑦,𝑧   𝑚,𝐸,𝑛,𝑥,𝑦,𝑧   𝑚,𝐻,𝑛,𝑥,𝑦,𝑧   𝑚,𝐹,𝑛,𝑥,𝑦,𝑧   𝑚,𝐺,𝑛,𝑥,𝑦,𝑧   𝑥,𝐽,𝑦,𝑧   𝜑,𝑚,𝑛,𝑥,𝑦,𝑧

Allowed substitution hints:   𝐶(𝑥, 𝑦, 𝑧, 𝑚, 𝑛)   · (𝑥, 𝑦, 𝑧, 𝑚, 𝑛)   1 (𝑥, 𝑦, 𝑧, 𝑚, 𝑛)   𝐼(𝑥, 𝑦, 𝑧, 𝑚, 𝑛)   𝐽(𝑚, 𝑛)   𝑂(𝑥, 𝑦, 𝑧, 𝑚, 𝑛)

Proof of Theorem isfuncd

Step	Hyp	Ref	Expression
1		isfuncd.1	. 2 ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)
2		isfuncd.2	. . . 4 ⊢ (𝜑 → 𝐺 Fn (𝐵 × 𝐵))
3		isfunc.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐷)
4	3	fvexi 6892	. . . . 5 ⊢ 𝐵 ∈ V
5	4, 4	xpex 7752	. . . 4 ⊢ (𝐵 × 𝐵) ∈ V
6		fnex 7216	. . . 4 ⊢ ((𝐺 Fn (𝐵 × 𝐵) ∧ (𝐵 × 𝐵) ∈ V) → 𝐺 ∈ V)
7	2, 5, 6	sylancl 598	. . 3 ⊢ (𝜑 → 𝐺 ∈ V)
8		isfuncd.3	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦)))
9		ovex 7446	. . . . . . 7 ⊢ ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∈ V
10		ovex 7446	. . . . . . 7 ⊢ (𝑥𝐻𝑦) ∈ V
11	9, 10	elmap 8878	. . . . . 6 ⊢ ((𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦)))
12	8, 11	sylibr 237	. . . . 5 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)))
13	12	ralrimivva 3205	. . . 4 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)))
14		fveq2 6878	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐺‘𝑧) = (𝐺‘⟨𝑥, 𝑦⟩))
15		df-ov 7416	. . . . . . 7 ⊢ (𝑥𝐺𝑦) = (𝐺‘⟨𝑥, 𝑦⟩)
16	14, 15	eqtr4di 2813	. . . . . 6 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐺‘𝑧) = (𝑥𝐺𝑦))
17		vex 3454	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
18		vex 3454	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
19	17, 18	op1std 7996	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (1st ‘𝑧) = 𝑥)
20	19	fveq2d 6882	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐹‘(1st ‘𝑧)) = (𝐹‘𝑥))
21	17, 18	op2ndd 7997	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
22	21	fveq2d 6882	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐹‘(2nd ‘𝑧)) = (𝐹‘𝑦))
23	20, 22	oveq12d 7431	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦)))
24		fveq2 6878	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻‘𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
25		df-ov 7416	. . . . . . . 8 ⊢ (𝑥𝐻𝑦) = (𝐻‘⟨𝑥, 𝑦⟩)
26	24, 25	eqtr4di 2813	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻‘𝑧) = (𝑥𝐻𝑦))
27	23, 26	oveq12d 7431	. . . . . 6 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)))
28	16, 27	eleq12d 2854	. . . . 5 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦))))
29	28	ralxp 5821	. . . 4 ⊢ (∀𝑧 ∈ (𝐵 × 𝐵)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)))
30	13, 29	sylibr 237	. . 3 ⊢ (𝜑 → ∀𝑧 ∈ (𝐵 × 𝐵)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
31		elixp2 8908	. . 3 ⊢ (𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑧 ∈ (𝐵 × 𝐵)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))))
32	7, 2, 30, 31	syl3anbrc 1362	. 2 ⊢ (𝜑 → 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))
33		isfuncd.4	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)))
34		isfuncd.5	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧))) → ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))
35	34	3expia 1139	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧)) → ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
36	35	3exp2 1373	. . . . . . 7 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → ((𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧)) → ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))))
37	36	imp43 433	. . . . . 6 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧)) → ((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
38	37	ralrimivv 3203	. . . . 5 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))
39	38	ralrimivva 3205	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))
40	33, 39	jca 521	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
41	40	ralrimiva 3154	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))
42		isfunc.c	. . 3 ⊢ 𝐶 = (Base‘𝐸)
43		isfunc.h	. . 3 ⊢ 𝐻 = (Hom ‘𝐷)
44		isfunc.j	. . 3 ⊢ 𝐽 = (Hom ‘𝐸)
45		isfunc.1	. . 3 ⊢ 1 = (Id‘𝐷)
46		isfunc.i	. . 3 ⊢ 𝐼 = (Id‘𝐸)
47		isfunc.x	. . 3 ⊢ · = (comp‘𝐷)
48		isfunc.o	. . 3 ⊢ 𝑂 = (comp‘𝐸)
49		isfunc.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ Cat)
50		isfunc.e	. . 3 ⊢ (𝜑 → 𝐸 ∈ Cat)
51	3, 42, 43, 44, 45, 46, 47, 48, 49, 50	isfunc 17953	. 2 ⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(⟨𝑥, 𝑦⟩ · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))
52	1, 32, 41, 51	mpbir3and 1361	1 ⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3076  Vcvv 3450  ⟨cop 4590   class class class wbr 5103   × cxp 5653   Fn wfn 6528  ⟶wf 6529  ‘cfv 6533  (class class class)co 7413  1^st c1st 7984  2^nd c2nd 7985   ↑_m cmap 8826  Xcixp 8904  Basecbs 17301  Hom chom 17353  compcco 17354  Catccat 17752  Idccid 17753   Func cfunc 17943

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 2732  ax-rep 5232  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7986  df-2nd 7987  df-map 8828  df-ixp 8905  df-func 17947

This theorem is used by:  funcoppc  17964  funcres  17985  catcisolem  18199  funcestrcsetc  18237  funcsetcestrc  18252  1stfcl  18285  2ndfcl  18286  prfcl  18291  evlfcl  18310  curf1cl  18316  curfcl  18320  hofcl  18347  funcringcsetcALTV2  49214  funcringcsetcALTV  49237  swapffunc  50208  fucofunc  50285  fucoppc  50336