Step | Hyp | Ref
| Expression |
1 | | prfcl.p |
. . . 4
⊢ 𝑃 = (𝐹 〈,〉F 𝐺) |
2 | | eqid 2826 |
. . . 4
⊢
(Base‘𝐶) =
(Base‘𝐶) |
3 | | eqid 2826 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
4 | | prfcl.c |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
5 | | prfcl.d |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (𝐶 Func 𝐸)) |
6 | 1, 2, 3, 4, 5 | prfval 17193 |
. . 3
⊢ (𝜑 → 𝑃 = 〈(𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉) |
7 | | fvex 6447 |
. . . . . . 7
⊢
(Base‘𝐶)
∈ V |
8 | 7 | mptex 6743 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) ∈ V |
9 | 7, 7 | mpt2ex 7511 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) ∈ V |
10 | 8, 9 | op1std 7439 |
. . . . 5
⊢ (𝑃 = 〈(𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉 → (1st
‘𝑃) = (𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉)) |
11 | 6, 10 | syl 17 |
. . . 4
⊢ (𝜑 → (1st
‘𝑃) = (𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉)) |
12 | 8, 9 | op2ndd 7440 |
. . . . 5
⊢ (𝑃 = 〈(𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉 → (2nd
‘𝑃) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))) |
13 | 6, 12 | syl 17 |
. . . 4
⊢ (𝜑 → (2nd
‘𝑃) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))) |
14 | 11, 13 | opeq12d 4632 |
. . 3
⊢ (𝜑 → 〈(1st
‘𝑃), (2nd
‘𝑃)〉 =
〈(𝑥 ∈
(Base‘𝐶) ↦
〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉), (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))〉) |
15 | 6, 14 | eqtr4d 2865 |
. 2
⊢ (𝜑 → 𝑃 = 〈(1st ‘𝑃), (2nd ‘𝑃)〉) |
16 | | prfcl.t |
. . . . 5
⊢ 𝑇 = (𝐷 ×c 𝐸) |
17 | | eqid 2826 |
. . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) |
18 | | eqid 2826 |
. . . . 5
⊢
(Base‘𝐸) =
(Base‘𝐸) |
19 | 16, 17, 18 | xpcbas 17172 |
. . . 4
⊢
((Base‘𝐷)
× (Base‘𝐸)) =
(Base‘𝑇) |
20 | | eqid 2826 |
. . . 4
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) |
21 | | eqid 2826 |
. . . 4
⊢
(Id‘𝐶) =
(Id‘𝐶) |
22 | | eqid 2826 |
. . . 4
⊢
(Id‘𝑇) =
(Id‘𝑇) |
23 | | eqid 2826 |
. . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) |
24 | | eqid 2826 |
. . . 4
⊢
(comp‘𝑇) =
(comp‘𝑇) |
25 | | funcrcl 16876 |
. . . . . 6
⊢ (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
26 | 4, 25 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) |
27 | 26 | simpld 490 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
28 | 26 | simprd 491 |
. . . . 5
⊢ (𝜑 → 𝐷 ∈ Cat) |
29 | | funcrcl 16876 |
. . . . . . 7
⊢ (𝐺 ∈ (𝐶 Func 𝐸) → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat)) |
30 | 5, 29 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐸 ∈ Cat)) |
31 | 30 | simprd 491 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ Cat) |
32 | 16, 28, 31 | xpccat 17184 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ Cat) |
33 | | relfunc 16875 |
. . . . . . . . . 10
⊢ Rel
(𝐶 Func 𝐷) |
34 | | 1st2ndbr 7480 |
. . . . . . . . . 10
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
35 | 33, 4, 34 | sylancr 583 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
36 | 2, 17, 35 | funcf1 16879 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
37 | 36 | ffvelrnda 6609 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
38 | | relfunc 16875 |
. . . . . . . . . 10
⊢ Rel
(𝐶 Func 𝐸) |
39 | | 1st2ndbr 7480 |
. . . . . . . . . 10
⊢ ((Rel
(𝐶 Func 𝐸) ∧ 𝐺 ∈ (𝐶 Func 𝐸)) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) |
40 | 38, 5, 39 | sylancr 583 |
. . . . . . . . 9
⊢ (𝜑 → (1st
‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) |
41 | 2, 18, 40 | funcf1 16879 |
. . . . . . . 8
⊢ (𝜑 → (1st
‘𝐺):(Base‘𝐶)⟶(Base‘𝐸)) |
42 | 41 | ffvelrnda 6609 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸)) |
43 | | opelxpi 5380 |
. . . . . . 7
⊢
((((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷) ∧ ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸)) → 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 ∈ ((Base‘𝐷) × (Base‘𝐸))) |
44 | 37, 42, 43 | syl2anc 581 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉 ∈ ((Base‘𝐷) × (Base‘𝐸))) |
45 | 44 | fmpttd 6635 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸))) |
46 | 11 | feq1d 6264 |
. . . . 5
⊢ (𝜑 → ((1st
‘𝑃):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸)) ↔ (𝑥 ∈ (Base‘𝐶) ↦ 〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸)))) |
47 | 45, 46 | mpbird 249 |
. . . 4
⊢ (𝜑 → (1st
‘𝑃):(Base‘𝐶)⟶((Base‘𝐷) × (Base‘𝐸))) |
48 | | eqid 2826 |
. . . . . 6
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) = (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) |
49 | | ovex 6938 |
. . . . . . 7
⊢ (𝑥(Hom ‘𝐶)𝑦) ∈ V |
50 | 49 | mptex 6743 |
. . . . . 6
⊢ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉) ∈ V |
51 | 48, 50 | fnmpt2i 7503 |
. . . . 5
⊢ (𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) Fn ((Base‘𝐶) × (Base‘𝐶)) |
52 | 13 | fneq1d 6215 |
. . . . 5
⊢ (𝜑 → ((2nd
‘𝑃) Fn
((Base‘𝐶) ×
(Base‘𝐶)) ↔
(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) Fn ((Base‘𝐶) × (Base‘𝐶)))) |
53 | 51, 52 | mpbiri 250 |
. . . 4
⊢ (𝜑 → (2nd
‘𝑃) Fn
((Base‘𝐶) ×
(Base‘𝐶))) |
54 | | eqid 2826 |
. . . . . . . . . 10
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
55 | 35 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
56 | | simprl 789 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶)) |
57 | | simprr 791 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) |
58 | 2, 3, 54, 55, 56, 57 | funcf2 16881 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) |
59 | 58 | ffvelrnda 6609 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐹)𝑦)‘ℎ) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) |
60 | | eqid 2826 |
. . . . . . . . . 10
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
61 | 40 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) |
62 | 2, 3, 60, 61, 56, 57 | funcf2 16881 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))) |
63 | 62 | ffvelrnda 6609 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑥(2nd ‘𝐺)𝑦)‘ℎ) ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))) |
64 | | opelxpi 5380 |
. . . . . . . 8
⊢ ((((𝑥(2nd ‘𝐹)𝑦)‘ℎ) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) ∧ ((𝑥(2nd ‘𝐺)𝑦)‘ℎ) ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))) → 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉 ∈ ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))) |
65 | 59, 63, 64 | syl2anc 581 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉 ∈ ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))) |
66 | 4 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷)) |
67 | 5 | adantr 474 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐶 Func 𝐸)) |
68 | 1, 2, 3, 66, 67, 56 | prf1 17194 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝑃)‘𝑥) = 〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) |
69 | 1, 2, 3, 66, 67, 57 | prf1 17194 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝑃)‘𝑦) = 〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉) |
70 | 68, 69 | oveq12d 6924 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)) = (〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(Hom ‘𝑇)〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉)) |
71 | 37 | adantrr 710 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
72 | 42 | adantrr 710 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸)) |
73 | 36 | ffvelrnda 6609 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) |
74 | 73 | adantrl 709 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) |
75 | 41 | ffvelrnda 6609 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (Base‘𝐶)) → ((1st ‘𝐺)‘𝑦) ∈ (Base‘𝐸)) |
76 | 75 | adantrl 709 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐺)‘𝑦) ∈ (Base‘𝐸)) |
77 | 16, 17, 18, 54, 60, 71, 72, 74, 76, 20 | xpchom2 17180 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉(Hom ‘𝑇)〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉) = ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))) |
78 | 70, 77 | eqtrd 2862 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)) = ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))) |
79 | 78 | adantr 474 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → (((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)) = ((((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦)) × (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦)))) |
80 | 65, 79 | eleqtrrd 2910 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) ∧ ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)) → 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉 ∈ (((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦))) |
81 | 80 | fmpttd 6635 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦))) |
82 | 13 | oveqd 6923 |
. . . . . . 7
⊢ (𝜑 → (𝑥(2nd ‘𝑃)𝑦) = (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))𝑦)) |
83 | 48 | ovmpt4g 7044 |
. . . . . . . 8
⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉) ∈ V) → (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))𝑦) = (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) |
84 | 50, 83 | mp3an3 1580 |
. . . . . . 7
⊢ ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(𝑥 ∈ (Base‘𝐶), 𝑦 ∈ (Base‘𝐶) ↦ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉))𝑦) = (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) |
85 | 82, 84 | sylan9eq 2882 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝑃)𝑦) = (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉)) |
86 | 85 | feq1d 6264 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((𝑥(2nd ‘𝑃)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)) ↔ (ℎ ∈ (𝑥(Hom ‘𝐶)𝑦) ↦ 〈((𝑥(2nd ‘𝐹)𝑦)‘ℎ), ((𝑥(2nd ‘𝐺)𝑦)‘ℎ)〉):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦)))) |
87 | 81, 86 | mpbird 249 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝑃)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝑃)‘𝑥)(Hom ‘𝑇)((1st ‘𝑃)‘𝑦))) |
88 | | eqid 2826 |
. . . . . . 7
⊢
(Id‘𝐷) =
(Id‘𝐷) |
89 | 35 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
90 | | simpr 479 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
91 | 2, 21, 88, 89, 90 | funcid 16883 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘((1st ‘𝐹)‘𝑥))) |
92 | | eqid 2826 |
. . . . . . 7
⊢
(Id‘𝐸) =
(Id‘𝐸) |
93 | 40 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) |
94 | 2, 21, 92, 93, 90 | funcid 16883 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))) |
95 | 91, 94 | opeq12d 4632 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 〈((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)), ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥))〉 = 〈((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)), ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))〉) |
96 | 4 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐹 ∈ (𝐶 Func 𝐷)) |
97 | 5 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐺 ∈ (𝐶 Func 𝐸)) |
98 | 27 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐶 ∈ Cat) |
99 | 2, 3, 21, 98, 90 | catidcl 16696 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝐶)‘𝑥) ∈ (𝑥(Hom ‘𝐶)𝑥)) |
100 | 1, 2, 3, 96, 97, 90, 90, 99 | prf2 17196 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝑃)𝑥)‘((Id‘𝐶)‘𝑥)) = 〈((𝑥(2nd ‘𝐹)𝑥)‘((Id‘𝐶)‘𝑥)), ((𝑥(2nd ‘𝐺)𝑥)‘((Id‘𝐶)‘𝑥))〉) |
101 | 1, 2, 3, 96, 97, 90 | prf1 17194 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((1st ‘𝑃)‘𝑥) = 〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) |
102 | 101 | fveq2d 6438 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘((1st ‘𝑃)‘𝑥)) = ((Id‘𝑇)‘〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉)) |
103 | 28 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐷 ∈ Cat) |
104 | 31 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐸 ∈ Cat) |
105 | 16, 103, 104, 17, 18, 88, 92, 22, 37, 42 | xpcid 17183 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) = 〈((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)), ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))〉) |
106 | 102, 105 | eqtrd 2862 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑇)‘((1st ‘𝑃)‘𝑥)) = 〈((Id‘𝐷)‘((1st ‘𝐹)‘𝑥)), ((Id‘𝐸)‘((1st ‘𝐺)‘𝑥))〉) |
107 | 95, 100, 106 | 3eqtr4d 2872 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥(2nd ‘𝑃)𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝑇)‘((1st ‘𝑃)‘𝑥))) |
108 | | eqid 2826 |
. . . . . . 7
⊢
(comp‘𝐷) =
(comp‘𝐷) |
109 | 35 | 3ad2ant1 1169 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
110 | | simp21 1269 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑥 ∈ (Base‘𝐶)) |
111 | | simp22 1270 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑦 ∈ (Base‘𝐶)) |
112 | | simp23 1271 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑧 ∈ (Base‘𝐶)) |
113 | | simp3l 1264 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
114 | | simp3r 1265 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧)) |
115 | 2, 3, 23, 108, 109, 110, 111, 112, 113, 114 | funcco 16884 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓))) |
116 | | eqid 2826 |
. . . . . . 7
⊢
(comp‘𝐸) =
(comp‘𝐸) |
117 | 5 | 3ad2ant1 1169 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐺 ∈ (𝐶 Func 𝐸)) |
118 | 38, 117, 39 | sylancr 583 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐺)(𝐶 Func 𝐸)(2nd ‘𝐺)) |
119 | 2, 3, 23, 116, 118, 110, 111, 112, 113, 114 | funcco 16884 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)(〈((1st ‘𝐺)‘𝑥), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐸)((1st ‘𝐺)‘𝑧))((𝑥(2nd ‘𝐺)𝑦)‘𝑓))) |
120 | 115, 119 | opeq12d 4632 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 〈((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)), ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))〉 = 〈(((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓)), (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)(〈((1st ‘𝐺)‘𝑥), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐸)((1st ‘𝐺)‘𝑧))((𝑥(2nd ‘𝐺)𝑦)‘𝑓))〉) |
121 | 4 | 3ad2ant1 1169 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐹 ∈ (𝐶 Func 𝐷)) |
122 | 27 | 3ad2ant1 1169 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 𝐶 ∈ Cat) |
123 | 2, 3, 23, 122, 110, 111, 112, 113, 114 | catcocl 16699 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓) ∈ (𝑥(Hom ‘𝐶)𝑧)) |
124 | 1, 2, 3, 121, 117, 110, 112, 123 | prf2 17196 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝑃)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = 〈((𝑥(2nd ‘𝐹)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)), ((𝑥(2nd ‘𝐺)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓))〉) |
125 | 1, 2, 3, 121, 117, 110 | prf1 17194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑥) = 〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉) |
126 | 1, 2, 3, 121, 117, 111 | prf1 17194 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑦) = 〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉) |
127 | 125, 126 | opeq12d 4632 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → 〈((1st
‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)〉 = 〈〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉, 〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉〉) |
128 | 1, 2, 3, 121, 117, 112 | prf1 17194 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝑃)‘𝑧) = 〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉) |
129 | 127, 128 | oveq12d 6924 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (〈((1st
‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)〉(comp‘𝑇)((1st ‘𝑃)‘𝑧)) = (〈〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉, 〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉〉(comp‘𝑇)〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉)) |
130 | 1, 2, 3, 121, 117, 111, 112, 114 | prf2 17196 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝑃)𝑧)‘𝑔) = 〈((𝑦(2nd ‘𝐹)𝑧)‘𝑔), ((𝑦(2nd ‘𝐺)𝑧)‘𝑔)〉) |
131 | 1, 2, 3, 121, 117, 110, 111, 113 | prf2 17196 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝑃)𝑦)‘𝑓) = 〈((𝑥(2nd ‘𝐹)𝑦)‘𝑓), ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)〉) |
132 | 129, 130,
131 | oveq123d 6927 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝑃)𝑧)‘𝑔)(〈((1st ‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)〉(comp‘𝑇)((1st ‘𝑃)‘𝑧))((𝑥(2nd ‘𝑃)𝑦)‘𝑓)) = (〈((𝑦(2nd ‘𝐹)𝑧)‘𝑔), ((𝑦(2nd ‘𝐺)𝑧)‘𝑔)〉(〈〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉, 〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉〉(comp‘𝑇)〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉)〈((𝑥(2nd ‘𝐹)𝑦)‘𝑓), ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)〉)) |
133 | 36 | 3ad2ant1 1169 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
134 | 133, 110 | ffvelrnd 6610 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
135 | 41 | 3ad2ant1 1169 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (1st ‘𝐺):(Base‘𝐶)⟶(Base‘𝐸)) |
136 | 135, 110 | ffvelrnd 6610 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑥) ∈ (Base‘𝐸)) |
137 | 133, 111 | ffvelrnd 6610 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) |
138 | 135, 111 | ffvelrnd 6610 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑦) ∈ (Base‘𝐸)) |
139 | 133, 112 | ffvelrnd 6610 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐹)‘𝑧) ∈ (Base‘𝐷)) |
140 | 135, 112 | ffvelrnd 6610 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((1st ‘𝐺)‘𝑧) ∈ (Base‘𝐸)) |
141 | 2, 3, 54, 109, 110, 111 | funcf2 16881 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) |
142 | 141, 113 | ffvelrnd 6610 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐹)𝑦)‘𝑓) ∈ (((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) |
143 | 2, 3, 60, 118, 110, 111 | funcf2 16881 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑥(2nd ‘𝐺)𝑦):(𝑥(Hom ‘𝐶)𝑦)⟶(((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))) |
144 | 143, 113 | ffvelrnd 6610 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝐺)𝑦)‘𝑓) ∈ (((1st ‘𝐺)‘𝑥)(Hom ‘𝐸)((1st ‘𝐺)‘𝑦))) |
145 | 2, 3, 54, 109, 111, 112 | funcf2 16881 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐹)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) |
146 | 145, 114 | ffvelrnd 6610 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐹)𝑧)‘𝑔) ∈ (((1st ‘𝐹)‘𝑦)(Hom ‘𝐷)((1st ‘𝐹)‘𝑧))) |
147 | 2, 3, 60, 118, 111, 112 | funcf2 16881 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (𝑦(2nd ‘𝐺)𝑧):(𝑦(Hom ‘𝐶)𝑧)⟶(((1st ‘𝐺)‘𝑦)(Hom ‘𝐸)((1st ‘𝐺)‘𝑧))) |
148 | 147, 114 | ffvelrnd 6610 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑦(2nd ‘𝐺)𝑧)‘𝑔) ∈ (((1st ‘𝐺)‘𝑦)(Hom ‘𝐸)((1st ‘𝐺)‘𝑧))) |
149 | 16, 17, 18, 54, 60, 134, 136, 137, 138, 108, 116, 24, 139, 140, 142, 144, 146, 148 | xpcco2 17181 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (〈((𝑦(2nd ‘𝐹)𝑧)‘𝑔), ((𝑦(2nd ‘𝐺)𝑧)‘𝑔)〉(〈〈((1st
‘𝐹)‘𝑥), ((1st ‘𝐺)‘𝑥)〉, 〈((1st ‘𝐹)‘𝑦), ((1st ‘𝐺)‘𝑦)〉〉(comp‘𝑇)〈((1st ‘𝐹)‘𝑧), ((1st ‘𝐺)‘𝑧)〉)〈((𝑥(2nd ‘𝐹)𝑦)‘𝑓), ((𝑥(2nd ‘𝐺)𝑦)‘𝑓)〉) = 〈(((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓)), (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)(〈((1st ‘𝐺)‘𝑥), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐸)((1st ‘𝐺)‘𝑧))((𝑥(2nd ‘𝐺)𝑦)‘𝑓))〉) |
150 | 132, 149 | eqtrd 2862 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → (((𝑦(2nd ‘𝑃)𝑧)‘𝑔)(〈((1st ‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)〉(comp‘𝑇)((1st ‘𝑃)‘𝑧))((𝑥(2nd ‘𝑃)𝑦)‘𝑓)) = 〈(((𝑦(2nd ‘𝐹)𝑧)‘𝑔)(〈((1st ‘𝐹)‘𝑥), ((1st ‘𝐹)‘𝑦)〉(comp‘𝐷)((1st ‘𝐹)‘𝑧))((𝑥(2nd ‘𝐹)𝑦)‘𝑓)), (((𝑦(2nd ‘𝐺)𝑧)‘𝑔)(〈((1st ‘𝐺)‘𝑥), ((1st ‘𝐺)‘𝑦)〉(comp‘𝐸)((1st ‘𝐺)‘𝑧))((𝑥(2nd ‘𝐺)𝑦)‘𝑓))〉) |
151 | 120, 124,
150 | 3eqtr4d 2872 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐶)𝑧))) → ((𝑥(2nd ‘𝑃)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝐶)𝑧)𝑓)) = (((𝑦(2nd ‘𝑃)𝑧)‘𝑔)(〈((1st ‘𝑃)‘𝑥), ((1st ‘𝑃)‘𝑦)〉(comp‘𝑇)((1st ‘𝑃)‘𝑧))((𝑥(2nd ‘𝑃)𝑦)‘𝑓))) |
152 | 2, 19, 3, 20, 21, 22, 23, 24, 27, 32, 47, 53, 87, 107, 151 | isfuncd 16878 |
. . 3
⊢ (𝜑 → (1st
‘𝑃)(𝐶 Func 𝑇)(2nd ‘𝑃)) |
153 | | df-br 4875 |
. . 3
⊢
((1st ‘𝑃)(𝐶 Func 𝑇)(2nd ‘𝑃) ↔ 〈(1st ‘𝑃), (2nd ‘𝑃)〉 ∈ (𝐶 Func 𝑇)) |
154 | 152, 153 | sylib 210 |
. 2
⊢ (𝜑 → 〈(1st
‘𝑃), (2nd
‘𝑃)〉 ∈
(𝐶 Func 𝑇)) |
155 | 15, 154 | eqeltrd 2907 |
1
⊢ (𝜑 → 𝑃 ∈ (𝐶 Func 𝑇)) |