| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | evlfcl.e | . . . . 5
⊢ 𝐸 = (𝐶 evalF 𝐷) | 
| 2 |  | evlfcl.c | . . . . 5
⊢ (𝜑 → 𝐶 ∈ Cat) | 
| 3 |  | evlfcl.d | . . . . 5
⊢ (𝜑 → 𝐷 ∈ Cat) | 
| 4 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) | 
| 5 |  | eqid 2736 | . . . . 5
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 6 |  | eqid 2736 | . . . . 5
⊢
(comp‘𝐷) =
(comp‘𝐷) | 
| 7 |  | eqid 2736 | . . . . 5
⊢ (𝐶 Nat 𝐷) = (𝐶 Nat 𝐷) | 
| 8 | 1, 2, 3, 4, 5, 6, 7 | evlfval 18263 | . . . 4
⊢ (𝜑 → 𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉) | 
| 9 |  | ovex 7465 | . . . . . 6
⊢ (𝐶 Func 𝐷) ∈ V | 
| 10 |  | fvex 6918 | . . . . . 6
⊢
(Base‘𝐶)
∈ V | 
| 11 | 9, 10 | mpoex 8105 | . . . . 5
⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)) ∈ V | 
| 12 | 9, 10 | xpex 7774 | . . . . . 6
⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∈ V | 
| 13 | 12, 12 | mpoex 8105 | . . . . 5
⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) ∈ V | 
| 14 | 11, 13 | opelvv 5724 | . . . 4
⊢
〈(𝑓 ∈
(𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉 ∈ (V ×
V) | 
| 15 | 8, 14 | eqeltrdi 2848 | . . 3
⊢ (𝜑 → 𝐸 ∈ (V × V)) | 
| 16 |  | 1st2nd2 8054 | . . 3
⊢ (𝐸 ∈ (V × V) →
𝐸 = 〈(1st
‘𝐸), (2nd
‘𝐸)〉) | 
| 17 | 15, 16 | syl 17 | . 2
⊢ (𝜑 → 𝐸 = 〈(1st ‘𝐸), (2nd ‘𝐸)〉) | 
| 18 |  | eqid 2736 | . . . . 5
⊢ (𝑄 ×c
𝐶) = (𝑄 ×c 𝐶) | 
| 19 |  | evlfcl.q | . . . . . 6
⊢ 𝑄 = (𝐶 FuncCat 𝐷) | 
| 20 | 19 | fucbas 18009 | . . . . 5
⊢ (𝐶 Func 𝐷) = (Base‘𝑄) | 
| 21 | 18, 20, 4 | xpcbas 18224 | . . . 4
⊢ ((𝐶 Func 𝐷) × (Base‘𝐶)) = (Base‘(𝑄 ×c 𝐶)) | 
| 22 |  | eqid 2736 | . . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) | 
| 23 |  | eqid 2736 | . . . 4
⊢ (Hom
‘(𝑄
×c 𝐶)) = (Hom ‘(𝑄 ×c 𝐶)) | 
| 24 |  | eqid 2736 | . . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) | 
| 25 |  | eqid 2736 | . . . 4
⊢
(Id‘(𝑄
×c 𝐶)) = (Id‘(𝑄 ×c 𝐶)) | 
| 26 |  | eqid 2736 | . . . 4
⊢
(Id‘𝐷) =
(Id‘𝐷) | 
| 27 |  | eqid 2736 | . . . 4
⊢
(comp‘(𝑄
×c 𝐶)) = (comp‘(𝑄 ×c 𝐶)) | 
| 28 | 19, 2, 3 | fuccat 18019 | . . . . 5
⊢ (𝜑 → 𝑄 ∈ Cat) | 
| 29 | 18, 28, 2 | xpccat 18236 | . . . 4
⊢ (𝜑 → (𝑄 ×c 𝐶) ∈ Cat) | 
| 30 |  | relfunc 17908 | . . . . . . . . . . 11
⊢ Rel
(𝐶 Func 𝐷) | 
| 31 |  | simpr 484 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → 𝑓 ∈ (𝐶 Func 𝐷)) | 
| 32 |  | 1st2ndbr 8068 | . . . . . . . . . . 11
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1st ‘𝑓)(𝐶 Func 𝐷)(2nd ‘𝑓)) | 
| 33 | 30, 31, 32 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1st ‘𝑓)(𝐶 Func 𝐷)(2nd ‘𝑓)) | 
| 34 | 4, 22, 33 | funcf1 17912 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → (1st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷)) | 
| 35 | 34 | ffvelcdmda 7103 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝑓)‘𝑥) ∈ (Base‘𝐷)) | 
| 36 | 35 | ralrimiva 3145 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑓 ∈ (𝐶 Func 𝐷)) → ∀𝑥 ∈ (Base‘𝐶)((1st ‘𝑓)‘𝑥) ∈ (Base‘𝐷)) | 
| 37 | 36 | ralrimiva 3145 | . . . . . 6
⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st ‘𝑓)‘𝑥) ∈ (Base‘𝐷)) | 
| 38 |  | eqid 2736 | . . . . . . 7
⊢ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)) | 
| 39 | 38 | fmpo 8094 | . . . . . 6
⊢
(∀𝑓 ∈
(𝐶 Func 𝐷)∀𝑥 ∈ (Base‘𝐶)((1st ‘𝑓)‘𝑥) ∈ (Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)) | 
| 40 | 37, 39 | sylib 218 | . . . . 5
⊢ (𝜑 → (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)) | 
| 41 | 11, 13 | op1std 8025 | . . . . . . 7
⊢ (𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉 → (1st
‘𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥))) | 
| 42 | 8, 41 | syl 17 | . . . . . 6
⊢ (𝜑 → (1st
‘𝐸) = (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥))) | 
| 43 | 42 | feq1d 6719 | . . . . 5
⊢ (𝜑 → ((1st
‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷) ↔ (𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷))) | 
| 44 | 40, 43 | mpbird 257 | . . . 4
⊢ (𝜑 → (1st
‘𝐸):((𝐶 Func 𝐷) × (Base‘𝐶))⟶(Base‘𝐷)) | 
| 45 |  | eqid 2736 | . . . . . 6
⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) | 
| 46 |  | ovex 7465 | . . . . . . . . 9
⊢ (𝑚(𝐶 Nat 𝐷)𝑛) ∈ V | 
| 47 |  | ovex 7465 | . . . . . . . . 9
⊢
((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ∈ V | 
| 48 | 46, 47 | mpoex 8105 | . . . . . . . 8
⊢ (𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) ∈ V | 
| 49 | 48 | csbex 5310 | . . . . . . 7
⊢
⦋(1st ‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) ∈ V | 
| 50 | 49 | csbex 5310 | . . . . . 6
⊢
⦋(1st ‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))) ∈ V | 
| 51 | 45, 50 | fnmpoi 8096 | . . . . 5
⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))) | 
| 52 | 11, 13 | op2ndd 8026 | . . . . . . 7
⊢ (𝐸 = 〈(𝑓 ∈ (𝐶 Func 𝐷), 𝑥 ∈ (Base‘𝐶) ↦ ((1st ‘𝑓)‘𝑥)), (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))〉 → (2nd
‘𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))) | 
| 53 | 8, 52 | syl 17 | . . . . . 6
⊢ (𝜑 → (2nd
‘𝐸) = (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔))))) | 
| 54 | 53 | fneq1d 6660 | . . . . 5
⊢ (𝜑 → ((2nd
‘𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))) ↔ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)), 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↦ ⦋(1st
‘𝑥) / 𝑚⦌⦋(1st
‘𝑦) / 𝑛⦌(𝑎 ∈ (𝑚(𝐶 Nat 𝐷)𝑛), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ ((𝑎‘(2nd ‘𝑦))(〈((1st
‘𝑚)‘(2nd ‘𝑥)), ((1st
‘𝑚)‘(2nd ‘𝑦))〉(comp‘𝐷)((1st ‘𝑛)‘(2nd
‘𝑦)))(((2nd ‘𝑥)(2nd ‘𝑚)(2nd ‘𝑦))‘𝑔)))) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶))))) | 
| 55 | 51, 54 | mpbiri 258 | . . . 4
⊢ (𝜑 → (2nd
‘𝐸) Fn (((𝐶 Func 𝐷) × (Base‘𝐶)) × ((𝐶 Func 𝐷) × (Base‘𝐶)))) | 
| 56 | 3 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat) | 
| 57 | 56 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝐷 ∈ Cat) | 
| 58 |  | simplrl 776 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷)) | 
| 59 | 30, 58, 32 | sylancr 587 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st ‘𝑓)(𝐶 Func 𝐷)(2nd ‘𝑓)) | 
| 60 | 4, 22, 59 | funcf1 17912 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷)) | 
| 61 | 60 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷)) | 
| 62 |  | simplrr 777 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶)) | 
| 63 | 62 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑢 ∈ (Base‘𝐶)) | 
| 64 | 61, 63 | ffvelcdmd 7104 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st ‘𝑓)‘𝑢) ∈ (Base‘𝐷)) | 
| 65 |  | simplrr 777 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑣 ∈ (Base‘𝐶)) | 
| 66 | 61, 65 | ffvelcdmd 7104 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st ‘𝑓)‘𝑣) ∈ (Base‘𝐷)) | 
| 67 |  | simprl 770 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑔 ∈ (𝐶 Func 𝐷)) | 
| 68 |  | 1st2ndbr 8068 | . . . . . . . . . . . . . . . . . . 19
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝑔 ∈ (𝐶 Func 𝐷)) → (1st ‘𝑔)(𝐶 Func 𝐷)(2nd ‘𝑔)) | 
| 69 | 30, 67, 68 | sylancr 587 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st ‘𝑔)(𝐶 Func 𝐷)(2nd ‘𝑔)) | 
| 70 | 4, 22, 69 | funcf1 17912 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (1st ‘𝑔):(Base‘𝐶)⟶(Base‘𝐷)) | 
| 71 | 70 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (1st ‘𝑔):(Base‘𝐶)⟶(Base‘𝐷)) | 
| 72 | 71, 65 | ffvelcdmd 7104 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((1st ‘𝑔)‘𝑣) ∈ (Base‘𝐷)) | 
| 73 |  | simprr 772 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝑣 ∈ (Base‘𝐶)) | 
| 74 | 4, 5, 24, 59, 62, 73 | funcf2 17914 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑢(2nd ‘𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑓)‘𝑣))) | 
| 75 | 74 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑢(2nd ‘𝑓)𝑣):(𝑢(Hom ‘𝐶)𝑣)⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑓)‘𝑣))) | 
| 76 |  | simprr 772 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ℎ ∈ (𝑢(Hom ‘𝐶)𝑣)) | 
| 77 | 75, 76 | ffvelcdmd 7104 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑢(2nd ‘𝑓)𝑣)‘ℎ) ∈ (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑓)‘𝑣))) | 
| 78 |  | simprl 770 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)) | 
| 79 | 7, 78 | nat1st2nd 18000 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → 𝑎 ∈ (〈(1st ‘𝑓), (2nd ‘𝑓)〉(𝐶 Nat 𝐷)〈(1st ‘𝑔), (2nd ‘𝑔)〉)) | 
| 80 | 7, 79, 4, 24, 65 | natcl 18002 | . . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → (𝑎‘𝑣) ∈ (((1st ‘𝑓)‘𝑣)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣))) | 
| 81 | 22, 24, 6, 57, 64, 66, 72, 77, 80 | catcocl 17729 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) ∧ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔) ∧ ℎ ∈ (𝑢(Hom ‘𝐶)𝑣))) → ((𝑎‘𝑣)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)〉(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣))) | 
| 82 | 81 | ralrimivva 3201 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ∀𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔)∀ℎ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎‘𝑣)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)〉(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣))) | 
| 83 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)〉(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ))) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)〉(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ))) | 
| 84 | 83 | fmpo 8094 | . . . . . . . . . . . . 13
⊢
(∀𝑎 ∈
(𝑓(𝐶 Nat 𝐷)𝑔)∀ℎ ∈ (𝑢(Hom ‘𝐶)𝑣)((𝑎‘𝑣)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)〉(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ)) ∈ (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)) ↔ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)〉(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣))) | 
| 85 | 82, 84 | sylib 218 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)〉(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣))) | 
| 86 | 2 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat) | 
| 87 |  | eqid 2736 | . . . . . . . . . . . . . 14
⊢
(〈𝑓, 𝑢〉(2nd
‘𝐸)〈𝑔, 𝑣〉) = (〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉) | 
| 88 | 1, 86, 56, 4, 5, 6,
7, 58, 67, 62, 73, 87 | evlf2 18264 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉) = (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)〉(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ)))) | 
| 89 | 88 | feq1d 6719 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)) ↔ (𝑎 ∈ (𝑓(𝐶 Nat 𝐷)𝑔), ℎ ∈ (𝑢(Hom ‘𝐶)𝑣) ↦ ((𝑎‘𝑣)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑣)〉(comp‘𝐷)((1st ‘𝑔)‘𝑣))((𝑢(2nd ‘𝑓)𝑣)‘ℎ))):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)))) | 
| 90 | 85, 89 | mpbird 257 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣))) | 
| 91 | 19, 7 | fuchom 18010 | . . . . . . . . . . . . 13
⊢ (𝐶 Nat 𝐷) = (Hom ‘𝑄) | 
| 92 | 18, 20, 4, 91, 5, 58, 62, 67, 73, 23 | xpchom2 18232 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (〈𝑓, 𝑢〉(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉) = ((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))) | 
| 93 | 1, 86, 56, 4, 58, 62 | evlf1 18266 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑓(1st ‘𝐸)𝑢) = ((1st ‘𝑓)‘𝑢)) | 
| 94 | 1, 86, 56, 4, 67, 73 | evlf1 18266 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (𝑔(1st ‘𝐸)𝑣) = ((1st ‘𝑔)‘𝑣)) | 
| 95 | 93, 94 | oveq12d 7450 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)) = (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣))) | 
| 96 | 92, 95 | feq23d 6730 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → ((〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉):(〈𝑓, 𝑢〉(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)) ↔ (〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉):((𝑓(𝐶 Nat 𝐷)𝑔) × (𝑢(Hom ‘𝐶)𝑣))⟶(((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑔)‘𝑣)))) | 
| 97 | 90, 96 | mpbird 257 | . . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) ∧ (𝑔 ∈ (𝐶 Func 𝐷) ∧ 𝑣 ∈ (Base‘𝐶))) → (〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉):(〈𝑓, 𝑢〉(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣))) | 
| 98 | 97 | ralrimivva 3201 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉):(〈𝑓, 𝑢〉(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣))) | 
| 99 | 98 | ralrimivva 3201 | . . . . . . . 8
⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉):(〈𝑓, 𝑢〉(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣))) | 
| 100 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑦 = 〈𝑔, 𝑣〉 → (𝑥(2nd ‘𝐸)𝑦) = (𝑥(2nd ‘𝐸)〈𝑔, 𝑣〉)) | 
| 101 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑦 = 〈𝑔, 𝑣〉 → (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) = (𝑥(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)) | 
| 102 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑦 = 〈𝑔, 𝑣〉 → ((1st ‘𝐸)‘𝑦) = ((1st ‘𝐸)‘〈𝑔, 𝑣〉)) | 
| 103 |  | df-ov 7435 | . . . . . . . . . . . . . 14
⊢ (𝑔(1st ‘𝐸)𝑣) = ((1st ‘𝐸)‘〈𝑔, 𝑣〉) | 
| 104 | 102, 103 | eqtr4di 2794 | . . . . . . . . . . . . 13
⊢ (𝑦 = 〈𝑔, 𝑣〉 → ((1st ‘𝐸)‘𝑦) = (𝑔(1st ‘𝐸)𝑣)) | 
| 105 | 104 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ (𝑦 = 〈𝑔, 𝑣〉 → (((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)) = (((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣))) | 
| 106 | 100, 101,
105 | feq123d 6724 | . . . . . . . . . . 11
⊢ (𝑦 = 〈𝑔, 𝑣〉 → ((𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)) ↔ (𝑥(2nd ‘𝐸)〈𝑔, 𝑣〉):(𝑥(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)))) | 
| 107 | 106 | ralxp 5851 | . . . . . . . . . 10
⊢
(∀𝑦 ∈
((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd ‘𝐸)〈𝑔, 𝑣〉):(𝑥(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣))) | 
| 108 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝑥 = 〈𝑓, 𝑢〉 → (𝑥(2nd ‘𝐸)〈𝑔, 𝑣〉) = (〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉)) | 
| 109 |  | oveq1 7439 | . . . . . . . . . . . 12
⊢ (𝑥 = 〈𝑓, 𝑢〉 → (𝑥(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉) = (〈𝑓, 𝑢〉(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)) | 
| 110 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 〈𝑓, 𝑢〉 → ((1st ‘𝐸)‘𝑥) = ((1st ‘𝐸)‘〈𝑓, 𝑢〉)) | 
| 111 |  | df-ov 7435 | . . . . . . . . . . . . . 14
⊢ (𝑓(1st ‘𝐸)𝑢) = ((1st ‘𝐸)‘〈𝑓, 𝑢〉) | 
| 112 | 110, 111 | eqtr4di 2794 | . . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝑓, 𝑢〉 → ((1st ‘𝐸)‘𝑥) = (𝑓(1st ‘𝐸)𝑢)) | 
| 113 | 112 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ (𝑥 = 〈𝑓, 𝑢〉 → (((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)) = ((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣))) | 
| 114 | 108, 109,
113 | feq123d 6724 | . . . . . . . . . . 11
⊢ (𝑥 = 〈𝑓, 𝑢〉 → ((𝑥(2nd ‘𝐸)〈𝑔, 𝑣〉):(𝑥(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)) ↔ (〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉):(〈𝑓, 𝑢〉(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)))) | 
| 115 | 114 | 2ralbidv 3220 | . . . . . . . . . 10
⊢ (𝑥 = 〈𝑓, 𝑢〉 → (∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(𝑥(2nd ‘𝐸)〈𝑔, 𝑣〉):(𝑥(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉):(〈𝑓, 𝑢〉(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)))) | 
| 116 | 107, 115 | bitrid 283 | . . . . . . . . 9
⊢ (𝑥 = 〈𝑓, 𝑢〉 → (∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)) ↔ ∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉):(〈𝑓, 𝑢〉(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣)))) | 
| 117 | 116 | ralxp 5851 | . . . . . . . 8
⊢
(∀𝑥 ∈
((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)∀𝑔 ∈ (𝐶 Func 𝐷)∀𝑣 ∈ (Base‘𝐶)(〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑔, 𝑣〉):(〈𝑓, 𝑢〉(Hom ‘(𝑄 ×c 𝐶))〈𝑔, 𝑣〉)⟶((𝑓(1st ‘𝐸)𝑢)(Hom ‘𝐷)(𝑔(1st ‘𝐸)𝑣))) | 
| 118 | 99, 117 | sylibr 234 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦))) | 
| 119 | 118 | r19.21bi 3250 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ∀𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))(𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦))) | 
| 120 | 119 | r19.21bi 3250 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → (𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦))) | 
| 121 | 120 | anasss 466 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)))) → (𝑥(2nd ‘𝐸)𝑦):(𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)⟶(((1st ‘𝐸)‘𝑥)(Hom ‘𝐷)((1st ‘𝐸)‘𝑦))) | 
| 122 | 28 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑄 ∈ Cat) | 
| 123 | 2 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat) | 
| 124 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Id‘𝑄) =
(Id‘𝑄) | 
| 125 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(Id‘𝐶) =
(Id‘𝐶) | 
| 126 |  | simprl 770 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑓 ∈ (𝐶 Func 𝐷)) | 
| 127 |  | simprr 772 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝑢 ∈ (Base‘𝐶)) | 
| 128 | 18, 122, 123, 20, 4, 124, 125, 25, 126, 127 | xpcid 18235 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘(𝑄 ×c 𝐶))‘〈𝑓, 𝑢〉) = 〈((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)〉) | 
| 129 | 128 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)‘((Id‘(𝑄 ×c 𝐶))‘〈𝑓, 𝑢〉)) = ((〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)‘〈((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)〉)) | 
| 130 |  | df-ov 7435 | . . . . . . . . 9
⊢
(((Id‘𝑄)‘𝑓)(〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)((Id‘𝐶)‘𝑢)) = ((〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)‘〈((Id‘𝑄)‘𝑓), ((Id‘𝐶)‘𝑢)〉) | 
| 131 | 129, 130 | eqtr4di 2794 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)‘((Id‘(𝑄 ×c 𝐶))‘〈𝑓, 𝑢〉)) = (((Id‘𝑄)‘𝑓)(〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)((Id‘𝐶)‘𝑢))) | 
| 132 | 3 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → 𝐷 ∈ Cat) | 
| 133 |  | eqid 2736 | . . . . . . . . 9
⊢
(〈𝑓, 𝑢〉(2nd
‘𝐸)〈𝑓, 𝑢〉) = (〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉) | 
| 134 | 20, 91, 124, 122, 126 | catidcl 17726 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) ∈ (𝑓(𝐶 Nat 𝐷)𝑓)) | 
| 135 | 4, 5, 125, 123, 127 | catidcl 17726 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐶)‘𝑢) ∈ (𝑢(Hom ‘𝐶)𝑢)) | 
| 136 | 1, 123, 132, 4, 5, 6, 7, 126, 126, 127, 127, 133, 134, 135 | evlf2val 18265 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)(〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)((Id‘𝐶)‘𝑢)) = ((((Id‘𝑄)‘𝑓)‘𝑢)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑢)〉(comp‘𝐷)((1st ‘𝑓)‘𝑢))((𝑢(2nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢)))) | 
| 137 | 30, 126, 32 | sylancr 587 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st ‘𝑓)(𝐶 Func 𝐷)(2nd ‘𝑓)) | 
| 138 | 4, 22, 137 | funcf1 17912 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (1st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷)) | 
| 139 | 138, 127 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((1st ‘𝑓)‘𝑢) ∈ (Base‘𝐷)) | 
| 140 | 22, 24, 26, 132, 139 | catidcl 17726 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢)) ∈ (((1st ‘𝑓)‘𝑢)(Hom ‘𝐷)((1st ‘𝑓)‘𝑢))) | 
| 141 | 22, 24, 26, 132, 139, 6, 139, 140 | catlid 17727 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑢)〉(comp‘𝐷)((1st ‘𝑓)‘𝑢))((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))) | 
| 142 | 19, 124, 26, 126 | fucid 18020 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝑄)‘𝑓) = ((Id‘𝐷) ∘ (1st ‘𝑓))) | 
| 143 | 142 | fveq1d 6907 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = (((Id‘𝐷) ∘ (1st ‘𝑓))‘𝑢)) | 
| 144 |  | fvco3 7007 | . . . . . . . . . . . 12
⊢
(((1st ‘𝑓):(Base‘𝐶)⟶(Base‘𝐷) ∧ 𝑢 ∈ (Base‘𝐶)) → (((Id‘𝐷) ∘ (1st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))) | 
| 145 | 138, 127,
144 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝐷) ∘ (1st ‘𝑓))‘𝑢) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))) | 
| 146 | 143, 145 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (((Id‘𝑄)‘𝑓)‘𝑢) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))) | 
| 147 | 4, 125, 26, 137, 127 | funcid 17916 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((𝑢(2nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢)) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))) | 
| 148 | 146, 147 | oveq12d 7450 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑢)〉(comp‘𝐷)((1st ‘𝑓)‘𝑢))((𝑢(2nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = (((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑢)〉(comp‘𝐷)((1st ‘𝑓)‘𝑢))((Id‘𝐷)‘((1st ‘𝑓)‘𝑢)))) | 
| 149 | 1, 123, 132, 4, 126, 127 | evlf1 18266 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → (𝑓(1st ‘𝐸)𝑢) = ((1st ‘𝑓)‘𝑢)) | 
| 150 | 149 | fveq2d 6909 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢)) = ((Id‘𝐷)‘((1st ‘𝑓)‘𝑢))) | 
| 151 | 141, 148,
150 | 3eqtr4d 2786 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((((Id‘𝑄)‘𝑓)‘𝑢)(〈((1st ‘𝑓)‘𝑢), ((1st ‘𝑓)‘𝑢)〉(comp‘𝐷)((1st ‘𝑓)‘𝑢))((𝑢(2nd ‘𝑓)𝑢)‘((Id‘𝐶)‘𝑢))) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢))) | 
| 152 | 131, 136,
151 | 3eqtrd 2780 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑓 ∈ (𝐶 Func 𝐷) ∧ 𝑢 ∈ (Base‘𝐶))) → ((〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)‘((Id‘(𝑄 ×c 𝐶))‘〈𝑓, 𝑢〉)) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢))) | 
| 153 | 152 | ralrimivva 3201 | . . . . . 6
⊢ (𝜑 → ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)‘((Id‘(𝑄 ×c 𝐶))‘〈𝑓, 𝑢〉)) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢))) | 
| 154 |  | id 22 | . . . . . . . . . 10
⊢ (𝑥 = 〈𝑓, 𝑢〉 → 𝑥 = 〈𝑓, 𝑢〉) | 
| 155 | 154, 154 | oveq12d 7450 | . . . . . . . . 9
⊢ (𝑥 = 〈𝑓, 𝑢〉 → (𝑥(2nd ‘𝐸)𝑥) = (〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)) | 
| 156 |  | fveq2 6905 | . . . . . . . . 9
⊢ (𝑥 = 〈𝑓, 𝑢〉 → ((Id‘(𝑄 ×c 𝐶))‘𝑥) = ((Id‘(𝑄 ×c 𝐶))‘〈𝑓, 𝑢〉)) | 
| 157 | 155, 156 | fveq12d 6912 | . . . . . . . 8
⊢ (𝑥 = 〈𝑓, 𝑢〉 → ((𝑥(2nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)‘((Id‘(𝑄 ×c 𝐶))‘〈𝑓, 𝑢〉))) | 
| 158 | 112 | fveq2d 6909 | . . . . . . . 8
⊢ (𝑥 = 〈𝑓, 𝑢〉 → ((Id‘𝐷)‘((1st ‘𝐸)‘𝑥)) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢))) | 
| 159 | 157, 158 | eqeq12d 2752 | . . . . . . 7
⊢ (𝑥 = 〈𝑓, 𝑢〉 → (((𝑥(2nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐸)‘𝑥)) ↔ ((〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)‘((Id‘(𝑄 ×c 𝐶))‘〈𝑓, 𝑢〉)) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢)))) | 
| 160 | 159 | ralxp 5851 | . . . . . 6
⊢
(∀𝑥 ∈
((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐸)‘𝑥)) ↔ ∀𝑓 ∈ (𝐶 Func 𝐷)∀𝑢 ∈ (Base‘𝐶)((〈𝑓, 𝑢〉(2nd ‘𝐸)〈𝑓, 𝑢〉)‘((Id‘(𝑄 ×c 𝐶))‘〈𝑓, 𝑢〉)) = ((Id‘𝐷)‘(𝑓(1st ‘𝐸)𝑢))) | 
| 161 | 153, 160 | sylibr 234 | . . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))((𝑥(2nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐸)‘𝑥))) | 
| 162 | 161 | r19.21bi 3250 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) → ((𝑥(2nd ‘𝐸)𝑥)‘((Id‘(𝑄 ×c 𝐶))‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐸)‘𝑥))) | 
| 163 | 2 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐶 ∈ Cat) | 
| 164 | 3 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝐷 ∈ Cat) | 
| 165 |  | simp21 1206 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) | 
| 166 |  | 1st2nd2 8054 | . . . . . . . . 9
⊢ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 167 | 165, 166 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 168 | 167, 165 | eqeltrrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) | 
| 169 |  | opelxp 5720 | . . . . . . 7
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st ‘𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑥) ∈ (Base‘𝐶))) | 
| 170 | 168, 169 | sylib 218 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝑥) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑥) ∈ (Base‘𝐶))) | 
| 171 |  | simp22 1207 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) | 
| 172 |  | 1st2nd2 8054 | . . . . . . . . 9
⊢ (𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) | 
| 173 | 171, 172 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑦 = 〈(1st ‘𝑦), (2nd ‘𝑦)〉) | 
| 174 | 173, 171 | eqeltrrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) | 
| 175 |  | opelxp 5720 | . . . . . . 7
⊢
(〈(1st ‘𝑦), (2nd ‘𝑦)〉 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st ‘𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑦) ∈ (Base‘𝐶))) | 
| 176 | 174, 175 | sylib 218 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝑦) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑦) ∈ (Base‘𝐶))) | 
| 177 |  | simp23 1208 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) | 
| 178 |  | 1st2nd2 8054 | . . . . . . . . 9
⊢ (𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 179 | 177, 178 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑧 = 〈(1st ‘𝑧), (2nd ‘𝑧)〉) | 
| 180 | 179, 177 | eqeltrrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) | 
| 181 |  | opelxp 5720 | . . . . . . 7
⊢
(〈(1st ‘𝑧), (2nd ‘𝑧)〉 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ↔ ((1st ‘𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑧) ∈ (Base‘𝐶))) | 
| 182 | 180, 181 | sylib 218 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝑧) ∈ (𝐶 Func 𝐷) ∧ (2nd ‘𝑧) ∈ (Base‘𝐶))) | 
| 183 |  | simp3l 1201 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦)) | 
| 184 | 18, 21, 91, 5, 23, 165, 171 | xpchom 18226 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) = (((1st ‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) | 
| 185 | 183, 184 | eleqtrd 2842 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 ∈ (((1st ‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) | 
| 186 |  | 1st2nd2 8054 | . . . . . . . . 9
⊢ (𝑓 ∈ (((1st
‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) | 
| 187 | 185, 186 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑓 = 〈(1st ‘𝑓), (2nd ‘𝑓)〉) | 
| 188 | 187, 185 | eqeltrrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 〈(1st ‘𝑓), (2nd ‘𝑓)〉 ∈ (((1st
‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) | 
| 189 |  | opelxp 5720 | . . . . . . 7
⊢
(〈(1st ‘𝑓), (2nd ‘𝑓)〉 ∈ (((1st ‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) ↔ ((1st ‘𝑓) ∈ ((1st
‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) ∧ (2nd ‘𝑓) ∈ ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) | 
| 190 | 188, 189 | sylib 218 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝑓) ∈ ((1st
‘𝑥)(𝐶 Nat 𝐷)(1st ‘𝑦)) ∧ (2nd ‘𝑓) ∈ ((2nd
‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) | 
| 191 |  | simp3r 1202 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧)) | 
| 192 | 18, 21, 91, 5, 23, 171, 177 | xpchom 18226 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧) = (((1st ‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧)))) | 
| 193 | 191, 192 | eleqtrd 2842 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 ∈ (((1st ‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧)))) | 
| 194 |  | 1st2nd2 8054 | . . . . . . . . 9
⊢ (𝑔 ∈ (((1st
‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) | 
| 195 | 193, 194 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 𝑔 = 〈(1st ‘𝑔), (2nd ‘𝑔)〉) | 
| 196 | 195, 193 | eqeltrrd 2841 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 〈(1st ‘𝑔), (2nd ‘𝑔)〉 ∈ (((1st
‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧)))) | 
| 197 |  | opelxp 5720 | . . . . . . 7
⊢
(〈(1st ‘𝑔), (2nd ‘𝑔)〉 ∈ (((1st ‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) × ((2nd ‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧))) ↔ ((1st ‘𝑔) ∈ ((1st
‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) ∧ (2nd ‘𝑔) ∈ ((2nd
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧)))) | 
| 198 | 196, 197 | sylib 218 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝑔) ∈ ((1st
‘𝑦)(𝐶 Nat 𝐷)(1st ‘𝑧)) ∧ (2nd ‘𝑔) ∈ ((2nd
‘𝑦)(Hom ‘𝐶)(2nd ‘𝑧)))) | 
| 199 | 1, 19, 163, 164, 7, 170, 176, 182, 190, 198 | evlfcllem 18267 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((〈(1st
‘𝑥), (2nd
‘𝑥)〉(2nd ‘𝐸)〈(1st
‘𝑧), (2nd
‘𝑧)〉)‘(〈(1st
‘𝑔), (2nd
‘𝑔)〉(〈〈(1st
‘𝑥), (2nd
‘𝑥)〉,
〈(1st ‘𝑦), (2nd ‘𝑦)〉〉(comp‘(𝑄 ×c 𝐶))〈(1st
‘𝑧), (2nd
‘𝑧)〉)〈(1st ‘𝑓), (2nd ‘𝑓)〉)) =
(((〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd ‘𝐸)〈(1st
‘𝑧), (2nd
‘𝑧)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉)(〈((1st ‘𝐸)‘〈(1st
‘𝑥), (2nd
‘𝑥)〉),
((1st ‘𝐸)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)〉(comp‘𝐷)((1st ‘𝐸)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉))((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝐸)〈(1st ‘𝑦), (2nd ‘𝑦)〉)‘〈(1st
‘𝑓), (2nd
‘𝑓)〉))) | 
| 200 | 167, 179 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd ‘𝐸)𝑧) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝐸)〈(1st ‘𝑧), (2nd ‘𝑧)〉)) | 
| 201 | 167, 173 | opeq12d 4880 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 〈𝑥, 𝑦〉 = 〈〈(1st
‘𝑥), (2nd
‘𝑥)〉,
〈(1st ‘𝑦), (2nd ‘𝑦)〉〉) | 
| 202 | 201, 179 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (〈𝑥, 𝑦〉(comp‘(𝑄 ×c 𝐶))𝑧) = (〈〈(1st ‘𝑥), (2nd ‘𝑥)〉, 〈(1st
‘𝑦), (2nd
‘𝑦)〉〉(comp‘(𝑄 ×c 𝐶))〈(1st
‘𝑧), (2nd
‘𝑧)〉)) | 
| 203 | 202, 195,
187 | oveq123d 7453 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘(𝑄 ×c 𝐶))𝑧)𝑓) = (〈(1st ‘𝑔), (2nd ‘𝑔)〉(〈〈(1st
‘𝑥), (2nd
‘𝑥)〉,
〈(1st ‘𝑦), (2nd ‘𝑦)〉〉(comp‘(𝑄 ×c 𝐶))〈(1st
‘𝑧), (2nd
‘𝑧)〉)〈(1st ‘𝑓), (2nd ‘𝑓)〉)) | 
| 204 | 200, 203 | fveq12d 6912 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝐸)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘(𝑄 ×c 𝐶))𝑧)𝑓)) = ((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝐸)〈(1st ‘𝑧), (2nd ‘𝑧)〉)‘(〈(1st
‘𝑔), (2nd
‘𝑔)〉(〈〈(1st
‘𝑥), (2nd
‘𝑥)〉,
〈(1st ‘𝑦), (2nd ‘𝑦)〉〉(comp‘(𝑄 ×c 𝐶))〈(1st
‘𝑧), (2nd
‘𝑧)〉)〈(1st ‘𝑓), (2nd ‘𝑓)〉))) | 
| 205 | 167 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝐸)‘𝑥) = ((1st ‘𝐸)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) | 
| 206 | 173 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝐸)‘𝑦) = ((1st ‘𝐸)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)) | 
| 207 | 205, 206 | opeq12d 4880 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → 〈((1st
‘𝐸)‘𝑥), ((1st ‘𝐸)‘𝑦)〉 = 〈((1st ‘𝐸)‘〈(1st
‘𝑥), (2nd
‘𝑥)〉),
((1st ‘𝐸)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)〉) | 
| 208 | 179 | fveq2d 6909 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((1st ‘𝐸)‘𝑧) = ((1st ‘𝐸)‘〈(1st ‘𝑧), (2nd ‘𝑧)〉)) | 
| 209 | 207, 208 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (〈((1st
‘𝐸)‘𝑥), ((1st ‘𝐸)‘𝑦)〉(comp‘𝐷)((1st ‘𝐸)‘𝑧)) = (〈((1st ‘𝐸)‘〈(1st
‘𝑥), (2nd
‘𝑥)〉),
((1st ‘𝐸)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)〉(comp‘𝐷)((1st ‘𝐸)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉))) | 
| 210 | 173, 179 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑦(2nd ‘𝐸)𝑧) = (〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd
‘𝐸)〈(1st ‘𝑧), (2nd ‘𝑧)〉)) | 
| 211 | 210, 195 | fveq12d 6912 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑦(2nd ‘𝐸)𝑧)‘𝑔) = ((〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd
‘𝐸)〈(1st ‘𝑧), (2nd ‘𝑧)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉)) | 
| 212 | 167, 173 | oveq12d 7450 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (𝑥(2nd ‘𝐸)𝑦) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝐸)〈(1st ‘𝑦), (2nd ‘𝑦)〉)) | 
| 213 | 212, 187 | fveq12d 6912 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝐸)𝑦)‘𝑓) = ((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝐸)〈(1st ‘𝑦), (2nd ‘𝑦)〉)‘〈(1st
‘𝑓), (2nd
‘𝑓)〉)) | 
| 214 | 209, 211,
213 | oveq123d 7453 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → (((𝑦(2nd ‘𝐸)𝑧)‘𝑔)(〈((1st ‘𝐸)‘𝑥), ((1st ‘𝐸)‘𝑦)〉(comp‘𝐷)((1st ‘𝐸)‘𝑧))((𝑥(2nd ‘𝐸)𝑦)‘𝑓)) = (((〈(1st ‘𝑦), (2nd ‘𝑦)〉(2nd
‘𝐸)〈(1st ‘𝑧), (2nd ‘𝑧)〉)‘〈(1st
‘𝑔), (2nd
‘𝑔)〉)(〈((1st ‘𝐸)‘〈(1st
‘𝑥), (2nd
‘𝑥)〉),
((1st ‘𝐸)‘〈(1st ‘𝑦), (2nd ‘𝑦)〉)〉(comp‘𝐷)((1st ‘𝐸)‘〈(1st
‘𝑧), (2nd
‘𝑧)〉))((〈(1st ‘𝑥), (2nd ‘𝑥)〉(2nd
‘𝐸)〈(1st ‘𝑦), (2nd ‘𝑦)〉)‘〈(1st
‘𝑓), (2nd
‘𝑓)〉))) | 
| 215 | 199, 204,
214 | 3eqtr4d 2786 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑦 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶)) ∧ 𝑧 ∈ ((𝐶 Func 𝐷) × (Base‘𝐶))) ∧ (𝑓 ∈ (𝑥(Hom ‘(𝑄 ×c 𝐶))𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘(𝑄 ×c 𝐶))𝑧))) → ((𝑥(2nd ‘𝐸)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘(𝑄 ×c 𝐶))𝑧)𝑓)) = (((𝑦(2nd ‘𝐸)𝑧)‘𝑔)(〈((1st ‘𝐸)‘𝑥), ((1st ‘𝐸)‘𝑦)〉(comp‘𝐷)((1st ‘𝐸)‘𝑧))((𝑥(2nd ‘𝐸)𝑦)‘𝑓))) | 
| 216 | 21, 22, 23, 24, 25, 26, 27, 6, 29, 3, 44, 55, 121, 162, 215 | isfuncd 17911 | . . 3
⊢ (𝜑 → (1st
‘𝐸)((𝑄 ×c
𝐶) Func 𝐷)(2nd ‘𝐸)) | 
| 217 |  | df-br 5143 | . . 3
⊢
((1st ‘𝐸)((𝑄 ×c 𝐶) Func 𝐷)(2nd ‘𝐸) ↔ 〈(1st ‘𝐸), (2nd ‘𝐸)〉 ∈ ((𝑄 ×c
𝐶) Func 𝐷)) | 
| 218 | 216, 217 | sylib 218 | . 2
⊢ (𝜑 → 〈(1st
‘𝐸), (2nd
‘𝐸)〉 ∈
((𝑄
×c 𝐶) Func 𝐷)) | 
| 219 | 17, 218 | eqeltrd 2840 | 1
⊢ (𝜑 → 𝐸 ∈ ((𝑄 ×c 𝐶) Func 𝐷)) |