Metamath Proof Explorer


Theorem isfuncd

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

Ref Expression
Hypotheses 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 isfuncd ( 𝜑𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )

Proof

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