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 𝐸 ) 𝐺 )