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