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 6919 | . . . . 5
⊢ 𝐵 ∈ V | 
| 5 | 4, 4 | xpex 7774 | . . . 4
⊢ (𝐵 × 𝐵) ∈ V | 
| 6 |  | fnex 7238 | . . . 4
⊢ ((𝐺 Fn (𝐵 × 𝐵) ∧ (𝐵 × 𝐵) ∈ V) → 𝐺 ∈ V) | 
| 7 | 2, 5, 6 | sylancl 586 | . . 3
⊢ (𝜑 → 𝐺 ∈ V) | 
| 8 |  | isfuncd.3 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦))) | 
| 9 |  | ovex 7465 | . . . . . . 7
⊢ ((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ∈ V | 
| 10 |  | ovex 7465 | . . . . . . 7
⊢ (𝑥𝐻𝑦) ∈ V | 
| 11 | 9, 10 | elmap 8912 | . . . . . 6
⊢ ((𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)) ↔ (𝑥𝐺𝑦):(𝑥𝐻𝑦)⟶((𝐹‘𝑥)𝐽(𝐹‘𝑦))) | 
| 12 | 8, 11 | sylibr 234 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦))) | 
| 13 | 12 | ralrimivva 3201 | . . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦))) | 
| 14 |  | fveq2 6905 | . . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝐺‘〈𝑥, 𝑦〉)) | 
| 15 |  | df-ov 7435 | . . . . . . 7
⊢ (𝑥𝐺𝑦) = (𝐺‘〈𝑥, 𝑦〉) | 
| 16 | 14, 15 | eqtr4di 2794 | . . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐺‘𝑧) = (𝑥𝐺𝑦)) | 
| 17 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑥 ∈ V | 
| 18 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑦 ∈ V | 
| 19 | 17, 18 | op1std 8025 | . . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (1st ‘𝑧) = 𝑥) | 
| 20 | 19 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘(1st ‘𝑧)) = (𝐹‘𝑥)) | 
| 21 | 17, 18 | op2ndd 8026 | . . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) | 
| 22 | 21 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐹‘(2nd ‘𝑧)) = (𝐹‘𝑦)) | 
| 23 | 20, 22 | oveq12d 7450 | . . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) = ((𝐹‘𝑥)𝐽(𝐹‘𝑦))) | 
| 24 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝐻‘〈𝑥, 𝑦〉)) | 
| 25 |  | df-ov 7435 | . . . . . . . 8
⊢ (𝑥𝐻𝑦) = (𝐻‘〈𝑥, 𝑦〉) | 
| 26 | 24, 25 | eqtr4di 2794 | . . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (𝐻‘𝑧) = (𝑥𝐻𝑦)) | 
| 27 | 23, 26 | oveq12d 7450 | . . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) = (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦))) | 
| 28 | 16, 27 | eleq12d 2834 | . . . . 5
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ((𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦)))) | 
| 29 | 28 | ralxp 5851 | . . . 4
⊢
(∀𝑧 ∈
(𝐵 × 𝐵)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝐺𝑦) ∈ (((𝐹‘𝑥)𝐽(𝐹‘𝑦)) ↑m (𝑥𝐻𝑦))) | 
| 30 | 13, 29 | sylibr 234 | . . 3
⊢ (𝜑 → ∀𝑧 ∈ (𝐵 × 𝐵)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) | 
| 31 |  | elixp2 8942 | . . 3
⊢ (𝐺 ∈ X𝑧 ∈
(𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ↔ (𝐺 ∈ V ∧ 𝐺 Fn (𝐵 × 𝐵) ∧ ∀𝑧 ∈ (𝐵 × 𝐵)(𝐺‘𝑧) ∈ (((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)))) | 
| 32 | 7, 2, 30, 31 | syl3anbrc 1343 | . 2
⊢ (𝜑 → 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧))) | 
| 33 |  | isfuncd.4 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥))) | 
| 34 |  | isfuncd.5 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) ∧ (𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧))) → ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) | 
| 35 | 34 | 3expia 1121 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧)) → ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) | 
| 36 | 35 | 3exp2 1354 | . . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐵 → (𝑦 ∈ 𝐵 → (𝑧 ∈ 𝐵 → ((𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧)) → ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))))))) | 
| 37 | 36 | imp43 427 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑚 ∈ (𝑥𝐻𝑦) ∧ 𝑛 ∈ (𝑦𝐻𝑧)) → ((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) | 
| 38 | 37 | ralrimivv 3199 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) | 
| 39 | 38 | ralrimivva 3201 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚))) | 
| 40 | 33, 39 | jca 511 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))) | 
| 41 | 40 | ralrimiva 3145 | . 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 17910 | . 2
⊢ (𝜑 → (𝐹(𝐷 Func 𝐸)𝐺 ↔ (𝐹:𝐵⟶𝐶 ∧ 𝐺 ∈ X𝑧 ∈ (𝐵 × 𝐵)(((𝐹‘(1st ‘𝑧))𝐽(𝐹‘(2nd ‘𝑧))) ↑m (𝐻‘𝑧)) ∧ ∀𝑥 ∈ 𝐵 (((𝑥𝐺𝑥)‘( 1 ‘𝑥)) = (𝐼‘(𝐹‘𝑥)) ∧ ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ∀𝑚 ∈ (𝑥𝐻𝑦)∀𝑛 ∈ (𝑦𝐻𝑧)((𝑥𝐺𝑧)‘(𝑛(〈𝑥, 𝑦〉 · 𝑧)𝑚)) = (((𝑦𝐺𝑧)‘𝑛)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉𝑂(𝐹‘𝑧))((𝑥𝐺𝑦)‘𝑚)))))) | 
| 52 | 1, 32, 41, 51 | mpbir3and 1342 | 1
⊢ (𝜑 → 𝐹(𝐷 Func 𝐸)𝐺) |