Step | Hyp | Ref
| Expression |
1 | | curfval.g |
. . . 4
⊢ 𝐺 = (〈𝐶, 𝐷〉 curryF 𝐹) |
2 | | curfval.a |
. . . 4
⊢ 𝐴 = (Base‘𝐶) |
3 | | curfval.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
4 | | curfval.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) |
5 | | curfval.f |
. . . 4
⊢ (𝜑 → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
6 | | curfval.b |
. . . 4
⊢ 𝐵 = (Base‘𝐷) |
7 | | curf1.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝐴) |
8 | | curf1.k |
. . . 4
⊢ 𝐾 = ((1st ‘𝐺)‘𝑋) |
9 | | eqid 2622 |
. . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
10 | | eqid 2622 |
. . . 4
⊢
(Id‘𝐶) =
(Id‘𝐶) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | curf1 16865 |
. . 3
⊢ (𝜑 → 𝐾 = 〈(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))〉) |
12 | | fvex 6201 |
. . . . . . . 8
⊢
(Base‘𝐷)
∈ V |
13 | 6, 12 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐵 ∈ V |
14 | 13 | mptex 6486 |
. . . . . 6
⊢ (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)) ∈ V |
15 | 13, 13 | mpt2ex 7247 |
. . . . . 6
⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔))) ∈ V |
16 | 14, 15 | op1std 7178 |
. . . . 5
⊢ (𝐾 = 〈(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))〉 → (1st ‘𝐾) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦))) |
17 | 11, 16 | syl 17 |
. . . 4
⊢ (𝜑 → (1st
‘𝐾) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦))) |
18 | 14, 15 | op2ndd 7179 |
. . . . 5
⊢ (𝐾 = 〈(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))〉 → (2nd ‘𝐾) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))) |
19 | 11, 18 | syl 17 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐾) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))) |
20 | 17, 19 | opeq12d 4410 |
. . 3
⊢ (𝜑 → 〈(1st
‘𝐾), (2nd
‘𝐾)〉 =
〈(𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)), (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))〉) |
21 | 11, 20 | eqtr4d 2659 |
. 2
⊢ (𝜑 → 𝐾 = 〈(1st ‘𝐾), (2nd ‘𝐾)〉) |
22 | | eqid 2622 |
. . . 4
⊢
(Base‘𝐸) =
(Base‘𝐸) |
23 | | eqid 2622 |
. . . 4
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
24 | | eqid 2622 |
. . . 4
⊢
(Id‘𝐷) =
(Id‘𝐷) |
25 | | eqid 2622 |
. . . 4
⊢
(Id‘𝐸) =
(Id‘𝐸) |
26 | | eqid 2622 |
. . . 4
⊢
(comp‘𝐷) =
(comp‘𝐷) |
27 | | eqid 2622 |
. . . 4
⊢
(comp‘𝐸) =
(comp‘𝐸) |
28 | | funcrcl 16523 |
. . . . . 6
⊢ (𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸) → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat)) |
29 | 5, 28 | syl 17 |
. . . . 5
⊢ (𝜑 → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat)) |
30 | 29 | simprd 479 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ Cat) |
31 | | eqid 2622 |
. . . . . . . . . 10
⊢ (𝐶 ×c
𝐷) = (𝐶 ×c 𝐷) |
32 | 31, 2, 6 | xpcbas 16818 |
. . . . . . . . 9
⊢ (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷)) |
33 | | relfunc 16522 |
. . . . . . . . . 10
⊢ Rel
((𝐶
×c 𝐷) Func 𝐸) |
34 | | 1st2ndbr 7217 |
. . . . . . . . . 10
⊢ ((Rel
((𝐶
×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹)) |
35 | 33, 5, 34 | sylancr 695 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐹)((𝐶 ×c
𝐷) Func 𝐸)(2nd ‘𝐹)) |
36 | 32, 22, 35 | funcf1 16526 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸)) |
37 | 36 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1st ‘𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸)) |
38 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑋 ∈ 𝐴) |
39 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
40 | 37, 38, 39 | fovrnd 6806 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (𝑋(1st ‘𝐹)𝑦) ∈ (Base‘𝐸)) |
41 | | eqid 2622 |
. . . . . 6
⊢ (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)) = (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)) |
42 | 40, 41 | fmptd 6385 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)):𝐵⟶(Base‘𝐸)) |
43 | 17 | feq1d 6030 |
. . . . 5
⊢ (𝜑 → ((1st
‘𝐾):𝐵⟶(Base‘𝐸) ↔ (𝑦 ∈ 𝐵 ↦ (𝑋(1st ‘𝐹)𝑦)):𝐵⟶(Base‘𝐸))) |
44 | 42, 43 | mpbird 247 |
. . . 4
⊢ (𝜑 → (1st
‘𝐾):𝐵⟶(Base‘𝐸)) |
45 | | eqid 2622 |
. . . . . 6
⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔))) = (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔))) |
46 | | ovex 6678 |
. . . . . . 7
⊢ (𝑦(Hom ‘𝐷)𝑧) ∈ V |
47 | 46 | mptex 6486 |
. . . . . 6
⊢ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)) ∈ V |
48 | 45, 47 | fnmpt2i 7239 |
. . . . 5
⊢ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔))) Fn (𝐵 × 𝐵) |
49 | 19 | fneq1d 5981 |
. . . . 5
⊢ (𝜑 → ((2nd
‘𝐾) Fn (𝐵 × 𝐵) ↔ (𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔))) Fn (𝐵 × 𝐵))) |
50 | 48, 49 | mpbiri 248 |
. . . 4
⊢ (𝜑 → (2nd
‘𝐾) Fn (𝐵 × 𝐵)) |
51 | | eqid 2622 |
. . . . . . . . 9
⊢ (Hom
‘(𝐶
×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷)) |
52 | 35 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹)) |
53 | 7 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑋 ∈ 𝐴) |
54 | | simplrl 800 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑦 ∈ 𝐵) |
55 | | opelxpi 5148 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 〈𝑋, 𝑦〉 ∈ (𝐴 × 𝐵)) |
56 | 53, 54, 55 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 〈𝑋, 𝑦〉 ∈ (𝐴 × 𝐵)) |
57 | | simplrr 801 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑧 ∈ 𝐵) |
58 | | opelxpi 5148 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → 〈𝑋, 𝑧〉 ∈ (𝐴 × 𝐵)) |
59 | 53, 57, 58 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 〈𝑋, 𝑧〉 ∈ (𝐴 × 𝐵)) |
60 | 32, 51, 23, 52, 56, 59 | funcf2 16528 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉):(〈𝑋, 𝑦〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑧〉)⟶(((1st ‘𝐹)‘〈𝑋, 𝑦〉)(Hom ‘𝐸)((1st ‘𝐹)‘〈𝑋, 𝑧〉))) |
61 | | eqid 2622 |
. . . . . . . . . 10
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
62 | 31, 32, 61, 9, 51, 56, 59 | xpchom 16820 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (〈𝑋, 𝑦〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑧〉) = (((1st
‘〈𝑋, 𝑦〉)(Hom ‘𝐶)(1st
‘〈𝑋, 𝑧〉)) ×
((2nd ‘〈𝑋, 𝑦〉)(Hom ‘𝐷)(2nd ‘〈𝑋, 𝑧〉)))) |
63 | 3 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐶 ∈ Cat) |
64 | 4 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐷 ∈ Cat) |
65 | 5 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
66 | 1, 2, 63, 64, 65, 6, 53, 8, 54 | curf11 16866 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦)) |
67 | | df-ov 6653 |
. . . . . . . . . . 11
⊢ (𝑋(1st ‘𝐹)𝑦) = ((1st ‘𝐹)‘〈𝑋, 𝑦〉) |
68 | 66, 67 | syl6req 2673 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐹)‘〈𝑋, 𝑦〉) = ((1st ‘𝐾)‘𝑦)) |
69 | 1, 2, 63, 64, 65, 6, 53, 8, 57 | curf11 16866 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐾)‘𝑧) = (𝑋(1st ‘𝐹)𝑧)) |
70 | | df-ov 6653 |
. . . . . . . . . . 11
⊢ (𝑋(1st ‘𝐹)𝑧) = ((1st ‘𝐹)‘〈𝑋, 𝑧〉) |
71 | 69, 70 | syl6req 2673 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘𝐹)‘〈𝑋, 𝑧〉) = ((1st ‘𝐾)‘𝑧)) |
72 | 68, 71 | oveq12d 6668 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((1st ‘𝐹)‘〈𝑋, 𝑦〉)(Hom ‘𝐸)((1st ‘𝐹)‘〈𝑋, 𝑧〉)) = (((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧))) |
73 | 62, 72 | feq23d 6040 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉):(〈𝑋, 𝑦〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑧〉)⟶(((1st ‘𝐹)‘〈𝑋, 𝑦〉)(Hom ‘𝐸)((1st ‘𝐹)‘〈𝑋, 𝑧〉)) ↔ (〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉):(((1st ‘〈𝑋, 𝑦〉)(Hom ‘𝐶)(1st ‘〈𝑋, 𝑧〉)) × ((2nd
‘〈𝑋, 𝑦〉)(Hom ‘𝐷)(2nd
‘〈𝑋, 𝑧〉)))⟶(((1st
‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))) |
74 | 60, 73 | mpbid 222 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉):(((1st ‘〈𝑋, 𝑦〉)(Hom ‘𝐶)(1st ‘〈𝑋, 𝑧〉)) × ((2nd
‘〈𝑋, 𝑦〉)(Hom ‘𝐷)(2nd
‘〈𝑋, 𝑧〉)))⟶(((1st
‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧))) |
75 | 2, 61, 10, 63, 53 | catidcl 16343 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋)) |
76 | | op1stg 7180 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (1st ‘〈𝑋, 𝑦〉) = 𝑋) |
77 | 53, 54, 76 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘〈𝑋, 𝑦〉) = 𝑋) |
78 | | op1stg 7180 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (1st ‘〈𝑋, 𝑧〉) = 𝑋) |
79 | 53, 57, 78 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘〈𝑋, 𝑧〉) = 𝑋) |
80 | 77, 79 | oveq12d 6668 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘〈𝑋, 𝑦〉)(Hom ‘𝐶)(1st ‘〈𝑋, 𝑧〉)) = (𝑋(Hom ‘𝐶)𝑋)) |
81 | 75, 80 | eleqtrrd 2704 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ ((1st ‘〈𝑋, 𝑦〉)(Hom ‘𝐶)(1st ‘〈𝑋, 𝑧〉))) |
82 | | simpr 477 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) |
83 | | op2ndg 7181 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → (2nd ‘〈𝑋, 𝑦〉) = 𝑦) |
84 | 53, 54, 83 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘〈𝑋, 𝑦〉) = 𝑦) |
85 | | op2ndg 7181 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵) → (2nd ‘〈𝑋, 𝑧〉) = 𝑧) |
86 | 53, 57, 85 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘〈𝑋, 𝑧〉) = 𝑧) |
87 | 84, 86 | oveq12d 6668 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ‘〈𝑋, 𝑦〉)(Hom ‘𝐷)(2nd ‘〈𝑋, 𝑧〉)) = (𝑦(Hom ‘𝐷)𝑧)) |
88 | 82, 87 | eleqtrrd 2704 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ ((2nd ‘〈𝑋, 𝑦〉)(Hom ‘𝐷)(2nd ‘〈𝑋, 𝑧〉))) |
89 | 74, 81, 88 | fovrnd 6806 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔) ∈ (((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧))) |
90 | | eqid 2622 |
. . . . . 6
⊢ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)) |
91 | 89, 90 | fmptd 6385 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)):(𝑦(Hom ‘𝐷)𝑧)⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧))) |
92 | 19 | oveqd 6667 |
. . . . . . 7
⊢ (𝜑 → (𝑦(2nd ‘𝐾)𝑧) = (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))𝑧)) |
93 | 45 | ovmpt4g 6783 |
. . . . . . . 8
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)) ∈ V) → (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔))) |
94 | 47, 93 | mp3an3 1413 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → (𝑦(𝑦 ∈ 𝐵, 𝑧 ∈ 𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔))) |
95 | 92, 94 | sylan9eq 2676 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(2nd ‘𝐾)𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔))) |
96 | 95 | feq1d 6030 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑦(2nd ‘𝐾)𝑧):(𝑦(Hom ‘𝐷)𝑧)⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)) ↔ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)):(𝑦(Hom ‘𝐷)𝑧)⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧)))) |
97 | 91, 96 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑦(2nd ‘𝐾)𝑧):(𝑦(Hom ‘𝐷)𝑧)⟶(((1st ‘𝐾)‘𝑦)(Hom ‘𝐸)((1st ‘𝐾)‘𝑧))) |
98 | 3 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐶 ∈ Cat) |
99 | 4 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐷 ∈ Cat) |
100 | | eqid 2622 |
. . . . . . . . 9
⊢
(Id‘(𝐶
×c 𝐷)) = (Id‘(𝐶 ×c 𝐷)) |
101 | 31, 98, 99, 2, 6, 10, 24, 100, 38, 39 | xpcid 16829 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘(𝐶 ×c 𝐷))‘〈𝑋, 𝑦〉) = 〈((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)〉) |
102 | 101 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑦〉)‘((Id‘(𝐶 ×c 𝐷))‘〈𝑋, 𝑦〉)) = ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑦〉)‘〈((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)〉)) |
103 | | df-ov 6653 |
. . . . . . 7
⊢
(((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑦〉)((Id‘𝐷)‘𝑦)) = ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑦〉)‘〈((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)〉) |
104 | 102, 103 | syl6eqr 2674 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑦〉)‘((Id‘(𝐶 ×c 𝐷))‘〈𝑋, 𝑦〉)) = (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑦〉)((Id‘𝐷)‘𝑦))) |
105 | 35 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹)) |
106 | 7, 55 | sylan 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 〈𝑋, 𝑦〉 ∈ (𝐴 × 𝐵)) |
107 | 32, 100, 25, 105, 106 | funcid 16530 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑦〉)‘((Id‘(𝐶 ×c 𝐷))‘〈𝑋, 𝑦〉)) = ((Id‘𝐸)‘((1st ‘𝐹)‘〈𝑋, 𝑦〉))) |
108 | 104, 107 | eqtr3d 2658 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑦〉)((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐹)‘〈𝑋, 𝑦〉))) |
109 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
110 | 6, 9, 24, 99, 39 | catidcl 16343 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘𝐷)‘𝑦) ∈ (𝑦(Hom ‘𝐷)𝑦)) |
111 | 1, 2, 98, 99, 109, 6, 38, 8, 39, 9, 10, 39, 110 | curf12 16867 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝑦(2nd ‘𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑦〉)((Id‘𝐷)‘𝑦))) |
112 | 1, 2, 98, 99, 109, 6, 38, 8, 39 | curf11 16866 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦)) |
113 | 112, 67 | syl6eq 2672 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1st ‘𝐾)‘𝑦) = ((1st ‘𝐹)‘〈𝑋, 𝑦〉)) |
114 | 113 | fveq2d 6195 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((Id‘𝐸)‘((1st ‘𝐾)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐹)‘〈𝑋, 𝑦〉))) |
115 | 108, 111,
114 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((𝑦(2nd ‘𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st ‘𝐾)‘𝑦))) |
116 | 7 | 3ad2ant1 1082 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋 ∈ 𝐴) |
117 | | simp21 1094 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑦 ∈ 𝐵) |
118 | | simp22 1095 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧 ∈ 𝐵) |
119 | | eqid 2622 |
. . . . . . . . . 10
⊢
(comp‘𝐶) =
(comp‘𝐶) |
120 | | eqid 2622 |
. . . . . . . . . 10
⊢
(comp‘(𝐶
×c 𝐷)) = (comp‘(𝐶 ×c 𝐷)) |
121 | | simp23 1096 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤 ∈ 𝐵) |
122 | 3 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat) |
123 | 2, 61, 10, 122, 116 | catidcl 16343 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋)) |
124 | | simp3l 1089 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) |
125 | | simp3r 1090 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)) |
126 | 31, 2, 6, 61, 9, 116, 117, 116, 118, 119, 26, 120, 116, 121, 123, 124, 123, 125 | xpcco2 16827 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈((Id‘𝐶)‘𝑋), ℎ〉(〈〈𝑋, 𝑦〉, 〈𝑋, 𝑧〉〉(comp‘(𝐶 ×c 𝐷))〈𝑋, 𝑤〉)〈((Id‘𝐶)‘𝑋), 𝑔〉) = 〈(((Id‘𝐶)‘𝑋)(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), (ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)〉) |
127 | 2, 61, 10, 122, 116, 119, 116, 123 | catlid 16344 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)) = ((Id‘𝐶)‘𝑋)) |
128 | 127 | opeq1d 4408 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈(((Id‘𝐶)‘𝑋)(〈𝑋, 𝑋〉(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), (ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)〉 = 〈((Id‘𝐶)‘𝑋), (ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)〉) |
129 | 126, 128 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈((Id‘𝐶)‘𝑋), ℎ〉(〈〈𝑋, 𝑦〉, 〈𝑋, 𝑧〉〉(comp‘(𝐶 ×c 𝐷))〈𝑋, 𝑤〉)〈((Id‘𝐶)‘𝑋), 𝑔〉) = 〈((Id‘𝐶)‘𝑋), (ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)〉) |
130 | 129 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘(〈((Id‘𝐶)‘𝑋), ℎ〉(〈〈𝑋, 𝑦〉, 〈𝑋, 𝑧〉〉(comp‘(𝐶 ×c 𝐷))〈𝑋, 𝑤〉)〈((Id‘𝐶)‘𝑋), 𝑔〉)) = ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), (ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)〉)) |
131 | | df-ov 6653 |
. . . . . . 7
⊢
(((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑤〉)(ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)) = ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), (ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)〉) |
132 | 130, 131 | syl6eqr 2674 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘(〈((Id‘𝐶)‘𝑋), ℎ〉(〈〈𝑋, 𝑦〉, 〈𝑋, 𝑧〉〉(comp‘(𝐶 ×c 𝐷))〈𝑋, 𝑤〉)〈((Id‘𝐶)‘𝑋), 𝑔〉)) = (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑤〉)(ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔))) |
133 | 35 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1st ‘𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd ‘𝐹)) |
134 | 116, 117,
55 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈𝑋, 𝑦〉 ∈ (𝐴 × 𝐵)) |
135 | 116, 118,
58 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈𝑋, 𝑧〉 ∈ (𝐴 × 𝐵)) |
136 | | opelxpi 5148 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) → 〈𝑋, 𝑤〉 ∈ (𝐴 × 𝐵)) |
137 | 116, 121,
136 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈𝑋, 𝑤〉 ∈ (𝐴 × 𝐵)) |
138 | | opelxpi 5148 |
. . . . . . . . 9
⊢
((((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 〈((Id‘𝐶)‘𝑋), 𝑔〉 ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧))) |
139 | 123, 124,
138 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈((Id‘𝐶)‘𝑋), 𝑔〉 ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧))) |
140 | 31, 2, 6, 61, 9, 116, 117, 116, 118, 51 | xpchom2 16826 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈𝑋, 𝑦〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑧〉) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧))) |
141 | 139, 140 | eleqtrrd 2704 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈((Id‘𝐶)‘𝑋), 𝑔〉 ∈ (〈𝑋, 𝑦〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑧〉)) |
142 | | opelxpi 5148 |
. . . . . . . . 9
⊢
((((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤)) → 〈((Id‘𝐶)‘𝑋), ℎ〉 ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤))) |
143 | 123, 125,
142 | syl2anc 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈((Id‘𝐶)‘𝑋), ℎ〉 ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤))) |
144 | 31, 2, 6, 61, 9, 116, 118, 116, 121, 51 | xpchom2 16826 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈𝑋, 𝑧〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑤〉) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤))) |
145 | 143, 144 | eleqtrrd 2704 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈((Id‘𝐶)‘𝑋), ℎ〉 ∈ (〈𝑋, 𝑧〉(Hom ‘(𝐶 ×c 𝐷))〈𝑋, 𝑤〉)) |
146 | 32, 51, 120, 27, 133, 134, 135, 137, 141, 145 | funcco 16531 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘(〈((Id‘𝐶)‘𝑋), ℎ〉(〈〈𝑋, 𝑦〉, 〈𝑋, 𝑧〉〉(comp‘(𝐶 ×c 𝐷))〈𝑋, 𝑤〉)〈((Id‘𝐶)‘𝑋), 𝑔〉)) = (((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), ℎ〉)(〈((1st ‘𝐹)‘〈𝑋, 𝑦〉), ((1st ‘𝐹)‘〈𝑋, 𝑧〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑋, 𝑤〉))((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)‘〈((Id‘𝐶)‘𝑋), 𝑔〉))) |
147 | 132, 146 | eqtr3d 2658 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑤〉)(ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)) = (((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), ℎ〉)(〈((1st ‘𝐹)‘〈𝑋, 𝑦〉), ((1st ‘𝐹)‘〈𝑋, 𝑧〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑋, 𝑤〉))((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)‘〈((Id‘𝐶)‘𝑋), 𝑔〉))) |
148 | 4 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat) |
149 | 5 | 3ad2ant1 1082 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) |
150 | 6, 9, 26, 148, 117, 118, 121, 124, 125 | catcocl 16346 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐷)𝑤)) |
151 | 1, 2, 122, 148, 149, 6, 116, 8, 117, 9, 10, 121, 150 | curf12 16867 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑤)‘(ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)) = (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑤〉)(ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔))) |
152 | 1, 2, 122, 148, 149, 6, 116, 8, 117 | curf11 16866 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑦) = (𝑋(1st ‘𝐹)𝑦)) |
153 | 152, 67 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑦) = ((1st ‘𝐹)‘〈𝑋, 𝑦〉)) |
154 | 1, 2, 122, 148, 149, 6, 116, 8, 118 | curf11 16866 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑧) = (𝑋(1st ‘𝐹)𝑧)) |
155 | 154, 70 | syl6eq 2672 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑧) = ((1st ‘𝐹)‘〈𝑋, 𝑧〉)) |
156 | 153, 155 | opeq12d 4410 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 〈((1st
‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)〉 = 〈((1st ‘𝐹)‘〈𝑋, 𝑦〉), ((1st ‘𝐹)‘〈𝑋, 𝑧〉)〉) |
157 | 1, 2, 122, 148, 149, 6, 116, 8, 121 | curf11 16866 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑤) = (𝑋(1st ‘𝐹)𝑤)) |
158 | | df-ov 6653 |
. . . . . . . 8
⊢ (𝑋(1st ‘𝐹)𝑤) = ((1st ‘𝐹)‘〈𝑋, 𝑤〉) |
159 | 157, 158 | syl6eq 2672 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st ‘𝐾)‘𝑤) = ((1st ‘𝐹)‘〈𝑋, 𝑤〉)) |
160 | 156, 159 | oveq12d 6668 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (〈((1st
‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)〉(comp‘𝐸)((1st ‘𝐾)‘𝑤)) = (〈((1st ‘𝐹)‘〈𝑋, 𝑦〉), ((1st ‘𝐹)‘〈𝑋, 𝑧〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑋, 𝑤〉))) |
161 | 1, 2, 122, 148, 149, 6, 116, 8, 118, 9, 10, 121, 125 | curf12 16867 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘𝐾)𝑤)‘ℎ) = (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)ℎ)) |
162 | | df-ov 6653 |
. . . . . . 7
⊢
(((Id‘𝐶)‘𝑋)(〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)ℎ) = ((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), ℎ〉) |
163 | 161, 162 | syl6eq 2672 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd ‘𝐾)𝑤)‘ℎ) = ((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), ℎ〉)) |
164 | 1, 2, 122, 148, 149, 6, 116, 8, 117, 9, 10, 118, 124 | curf12 16867 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑧)‘𝑔) = (((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔)) |
165 | | df-ov 6653 |
. . . . . . 7
⊢
(((Id‘𝐶)‘𝑋)(〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)𝑔) = ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)‘〈((Id‘𝐶)‘𝑋), 𝑔〉) |
166 | 164, 165 | syl6eq 2672 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑧)‘𝑔) = ((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)‘〈((Id‘𝐶)‘𝑋), 𝑔〉)) |
167 | 160, 163,
166 | oveq123d 6671 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd ‘𝐾)𝑤)‘ℎ)(〈((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)〉(comp‘𝐸)((1st ‘𝐾)‘𝑤))((𝑦(2nd ‘𝐾)𝑧)‘𝑔)) = (((〈𝑋, 𝑧〉(2nd ‘𝐹)〈𝑋, 𝑤〉)‘〈((Id‘𝐶)‘𝑋), ℎ〉)(〈((1st ‘𝐹)‘〈𝑋, 𝑦〉), ((1st ‘𝐹)‘〈𝑋, 𝑧〉)〉(comp‘𝐸)((1st ‘𝐹)‘〈𝑋, 𝑤〉))((〈𝑋, 𝑦〉(2nd ‘𝐹)〈𝑋, 𝑧〉)‘〈((Id‘𝐶)‘𝑋), 𝑔〉))) |
168 | 147, 151,
167 | 3eqtr4d 2666 |
. . . 4
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ℎ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd ‘𝐾)𝑤)‘(ℎ(〈𝑦, 𝑧〉(comp‘𝐷)𝑤)𝑔)) = (((𝑧(2nd ‘𝐾)𝑤)‘ℎ)(〈((1st ‘𝐾)‘𝑦), ((1st ‘𝐾)‘𝑧)〉(comp‘𝐸)((1st ‘𝐾)‘𝑤))((𝑦(2nd ‘𝐾)𝑧)‘𝑔))) |
169 | 6, 22, 9, 23, 24, 25, 26, 27, 4, 30, 44, 50, 97, 115, 168 | isfuncd 16525 |
. . 3
⊢ (𝜑 → (1st
‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾)) |
170 | | df-br 4654 |
. . 3
⊢
((1st ‘𝐾)(𝐷 Func 𝐸)(2nd ‘𝐾) ↔ 〈(1st ‘𝐾), (2nd ‘𝐾)〉 ∈ (𝐷 Func 𝐸)) |
171 | 169, 170 | sylib 208 |
. 2
⊢ (𝜑 → 〈(1st
‘𝐾), (2nd
‘𝐾)〉 ∈
(𝐷 Func 𝐸)) |
172 | 21, 171 | eqeltrd 2701 |
1
⊢ (𝜑 → 𝐾 ∈ (𝐷 Func 𝐸)) |