Step | Hyp | Ref
| Expression |
1 | | 1stfcl.t |
. . . 4
⊢ 𝑇 = (𝐶 ×c 𝐷) |
2 | | eqid 2740 |
. . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) |
3 | | eqid 2740 |
. . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) |
4 | 1, 2, 3 | xpcbas 17891 |
. . . 4
⊢
((Base‘𝐶)
× (Base‘𝐷)) =
(Base‘𝑇) |
5 | | eqid 2740 |
. . . 4
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) |
6 | | 1stfcl.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) |
7 | | 1stfcl.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) |
8 | | 1stfcl.p |
. . . 4
⊢ 𝑃 = (𝐶 1stF 𝐷) |
9 | 1, 4, 5, 6, 7, 8 | 1stfval 17904 |
. . 3
⊢ (𝜑 → 𝑃 = 〈(1st ↾
((Base‘𝐶) ×
(Base‘𝐷))), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦)))〉) |
10 | | fo1st 7842 |
. . . . . . . 8
⊢
1st :V–onto→V |
11 | | fofun 6686 |
. . . . . . . 8
⊢
(1st :V–onto→V → Fun 1st ) |
12 | 10, 11 | ax-mp 5 |
. . . . . . 7
⊢ Fun
1st |
13 | | fvex 6782 |
. . . . . . . 8
⊢
(Base‘𝐶)
∈ V |
14 | | fvex 6782 |
. . . . . . . 8
⊢
(Base‘𝐷)
∈ V |
15 | 13, 14 | xpex 7595 |
. . . . . . 7
⊢
((Base‘𝐶)
× (Base‘𝐷))
∈ V |
16 | | resfunexg 7086 |
. . . . . . 7
⊢ ((Fun
1st ∧ ((Base‘𝐶) × (Base‘𝐷)) ∈ V) → (1st ↾
((Base‘𝐶) ×
(Base‘𝐷))) ∈
V) |
17 | 12, 15, 16 | mp2an 689 |
. . . . . 6
⊢
(1st ↾ ((Base‘𝐶) × (Base‘𝐷))) ∈ V |
18 | 15, 15 | mpoex 7911 |
. . . . . 6
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦))) ∈ V |
19 | 17, 18 | op2ndd 7833 |
. . . . 5
⊢ (𝑃 = 〈(1st ↾
((Base‘𝐶) ×
(Base‘𝐷))), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦)))〉 → (2nd ‘𝑃) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦)))) |
20 | 9, 19 | syl 17 |
. . . 4
⊢ (𝜑 → (2nd
‘𝑃) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦)))) |
21 | 20 | opeq2d 4817 |
. . 3
⊢ (𝜑 → 〈(1st
↾ ((Base‘𝐶)
× (Base‘𝐷))),
(2nd ‘𝑃)〉 = 〈(1st ↾
((Base‘𝐶) ×
(Base‘𝐷))), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦)))〉) |
22 | 9, 21 | eqtr4d 2783 |
. 2
⊢ (𝜑 → 𝑃 = 〈(1st ↾
((Base‘𝐶) ×
(Base‘𝐷))),
(2nd ‘𝑃)〉) |
23 | | eqid 2740 |
. . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
24 | | eqid 2740 |
. . . 4
⊢
(Id‘𝑇) =
(Id‘𝑇) |
25 | | eqid 2740 |
. . . 4
⊢
(Id‘𝐶) =
(Id‘𝐶) |
26 | | eqid 2740 |
. . . 4
⊢
(comp‘𝑇) =
(comp‘𝑇) |
27 | | eqid 2740 |
. . . 4
⊢
(comp‘𝐶) =
(comp‘𝐶) |
28 | 1, 6, 7 | xpccat 17903 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ Cat) |
29 | | f1stres 7846 |
. . . . 5
⊢
(1st ↾ ((Base‘𝐶) × (Base‘𝐷))):((Base‘𝐶) × (Base‘𝐷))⟶(Base‘𝐶) |
30 | 29 | a1i 11 |
. . . 4
⊢ (𝜑 → (1st ↾
((Base‘𝐶) ×
(Base‘𝐷))):((Base‘𝐶) × (Base‘𝐷))⟶(Base‘𝐶)) |
31 | | eqid 2740 |
. . . . . 6
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦))) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦))) |
32 | | ovex 7302 |
. . . . . . 7
⊢ (𝑥(Hom ‘𝑇)𝑦) ∈ V |
33 | | resfunexg 7086 |
. . . . . . 7
⊢ ((Fun
1st ∧ (𝑥(Hom
‘𝑇)𝑦) ∈ V) → (1st ↾
(𝑥(Hom ‘𝑇)𝑦)) ∈ V) |
34 | 12, 32, 33 | mp2an 689 |
. . . . . 6
⊢
(1st ↾ (𝑥(Hom ‘𝑇)𝑦)) ∈ V |
35 | 31, 34 | fnmpoi 7901 |
. . . . 5
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦))) Fn (((Base‘𝐶) × (Base‘𝐷)) × ((Base‘𝐶) × (Base‘𝐷))) |
36 | 20 | fneq1d 6523 |
. . . . 5
⊢ (𝜑 → ((2nd
‘𝑃) Fn
(((Base‘𝐶) ×
(Base‘𝐷)) ×
((Base‘𝐶) ×
(Base‘𝐷))) ↔
(𝑥 ∈
((Base‘𝐶) ×
(Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st
↾ (𝑥(Hom ‘𝑇)𝑦))) Fn (((Base‘𝐶) × (Base‘𝐷)) × ((Base‘𝐶) × (Base‘𝐷))))) |
37 | 35, 36 | mpbiri 257 |
. . . 4
⊢ (𝜑 → (2nd
‘𝑃) Fn
(((Base‘𝐶) ×
(Base‘𝐷)) ×
((Base‘𝐶) ×
(Base‘𝐷)))) |
38 | | f1stres 7846 |
. . . . . 6
⊢
(1st ↾ (((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))):(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))⟶((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) |
39 | 6 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → 𝐶 ∈ Cat) |
40 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → 𝐷 ∈ Cat) |
41 | | simprl 768 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
42 | | simprr 770 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
43 | 1, 4, 5, 39, 40, 8, 41, 42 | 1stf2 17906 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd ‘𝑃)𝑦) = (1st ↾ (𝑥(Hom ‘𝑇)𝑦))) |
44 | | eqid 2740 |
. . . . . . . . . 10
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
45 | 1, 4, 23, 44, 5, 41, 42 | xpchom 17893 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(Hom ‘𝑇)𝑦) = (((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))) |
46 | 45 | reseq2d 5889 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (1st ↾ (𝑥(Hom ‘𝑇)𝑦)) = (1st ↾
(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦))))) |
47 | 43, 46 | eqtrd 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd ‘𝑃)𝑦) = (1st ↾ (((1st
‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd
‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦))))) |
48 | 47 | feq1d 6582 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → ((𝑥(2nd ‘𝑃)𝑦):(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))⟶((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) ↔ (1st ↾
(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))):(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))⟶((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)))) |
49 | 38, 48 | mpbiri 257 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd ‘𝑃)𝑦):(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))⟶((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦))) |
50 | | fvres 6788 |
. . . . . . . 8
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → ((1st
↾ ((Base‘𝐶)
× (Base‘𝐷)))‘𝑥) = (1st ‘𝑥)) |
51 | 50 | ad2antrl 725 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → ((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥) = (1st ‘𝑥)) |
52 | | fvres 6788 |
. . . . . . . 8
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) → ((1st
↾ ((Base‘𝐶)
× (Base‘𝐷)))‘𝑦) = (1st ‘𝑦)) |
53 | 52 | ad2antll 726 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → ((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦) = (1st ‘𝑦)) |
54 | 51, 53 | oveq12d 7287 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥)(Hom ‘𝐶)((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦)) = ((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦))) |
55 | 45, 54 | feq23d 6592 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → ((𝑥(2nd ‘𝑃)𝑦):(𝑥(Hom ‘𝑇)𝑦)⟶(((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥)(Hom ‘𝐶)((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦)) ↔ (𝑥(2nd ‘𝑃)𝑦):(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))⟶((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)))) |
56 | 49, 55 | mpbird 256 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd ‘𝑃)𝑦):(𝑥(Hom ‘𝑇)𝑦)⟶(((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥)(Hom ‘𝐶)((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦))) |
57 | 28 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝑇 ∈ Cat) |
58 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
59 | 4, 5, 24, 57, 58 | catidcl 17387 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘𝑥) ∈ (𝑥(Hom ‘𝑇)𝑥)) |
60 | 59 | fvresd 6789 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((1st ↾ (𝑥(Hom ‘𝑇)𝑥))‘((Id‘𝑇)‘𝑥)) = (1st ‘((Id‘𝑇)‘𝑥))) |
61 | | 1st2nd2 7861 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
62 | 61 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
63 | 62 | fveq2d 6773 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘𝑥) = ((Id‘𝑇)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
64 | 6 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝐶 ∈ Cat) |
65 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝐷 ∈ Cat) |
66 | | eqid 2740 |
. . . . . . . . 9
⊢
(Id‘𝐷) =
(Id‘𝐷) |
67 | | xp1st 7854 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → (1st
‘𝑥) ∈
(Base‘𝐶)) |
68 | 67 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (1st ‘𝑥) ∈ (Base‘𝐶)) |
69 | | xp2nd 7855 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → (2nd
‘𝑥) ∈
(Base‘𝐷)) |
70 | 69 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (2nd ‘𝑥) ∈ (Base‘𝐷)) |
71 | 1, 64, 65, 2, 3, 25, 66, 24, 68, 70 | xpcid 17902 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) =
〈((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐷)‘(2nd ‘𝑥))〉) |
72 | 63, 71 | eqtrd 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘𝑥) = 〈((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐷)‘(2nd ‘𝑥))〉) |
73 | | fvex 6782 |
. . . . . . . 8
⊢
((Id‘𝐶)‘(1st ‘𝑥)) ∈ V |
74 | | fvex 6782 |
. . . . . . . 8
⊢
((Id‘𝐷)‘(2nd ‘𝑥)) ∈ V |
75 | 73, 74 | op1std 7832 |
. . . . . . 7
⊢
(((Id‘𝑇)‘𝑥) = 〈((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐷)‘(2nd ‘𝑥))〉 → (1st
‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐶)‘(1st ‘𝑥))) |
76 | 72, 75 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (1st
‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐶)‘(1st ‘𝑥))) |
77 | 60, 76 | eqtrd 2780 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((1st ↾ (𝑥(Hom ‘𝑇)𝑥))‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐶)‘(1st ‘𝑥))) |
78 | 1, 4, 5, 64, 65, 8, 58, 58 | 1stf2 17906 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (𝑥(2nd ‘𝑃)𝑥) = (1st ↾ (𝑥(Hom ‘𝑇)𝑥))) |
79 | 78 | fveq1d 6771 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((𝑥(2nd ‘𝑃)𝑥)‘((Id‘𝑇)‘𝑥)) = ((1st ↾ (𝑥(Hom ‘𝑇)𝑥))‘((Id‘𝑇)‘𝑥))) |
80 | 50 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥) = (1st ‘𝑥)) |
81 | 80 | fveq2d 6773 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝐶)‘((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥)) = ((Id‘𝐶)‘(1st ‘𝑥))) |
82 | 77, 79, 81 | 3eqtr4d 2790 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((𝑥(2nd ‘𝑃)𝑥)‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐶)‘((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥))) |
83 | 28 | 3ad2ant1 1132 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑇 ∈ Cat) |
84 | | simp21 1205 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
85 | | simp22 1206 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
86 | | simp23 1207 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) |
87 | | simp3l 1200 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦)) |
88 | | simp3r 1201 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧)) |
89 | 4, 5, 26, 83, 84, 85, 86, 87, 88 | catcocl 17390 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓) ∈ (𝑥(Hom ‘𝑇)𝑧)) |
90 | 89 | fvresd 6789 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾ (𝑥(Hom ‘𝑇)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓)) = (1st ‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓))) |
91 | 1, 4, 5, 26, 84, 85, 86, 87, 88, 27 | xpcco1st 17897 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (1st ‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓)) = ((1st ‘𝑔)(〈(1st
‘𝑥), (1st
‘𝑦)〉(comp‘𝐶)(1st ‘𝑧))(1st ‘𝑓))) |
92 | 90, 91 | eqtrd 2780 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾ (𝑥(Hom ‘𝑇)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓)) = ((1st ‘𝑔)(〈(1st
‘𝑥), (1st
‘𝑦)〉(comp‘𝐶)(1st ‘𝑧))(1st ‘𝑓))) |
93 | 6 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝐶 ∈ Cat) |
94 | 7 | 3ad2ant1 1132 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝐷 ∈ Cat) |
95 | 1, 4, 5, 93, 94, 8, 84, 86 | 1stf2 17906 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑥(2nd ‘𝑃)𝑧) = (1st ↾ (𝑥(Hom ‘𝑇)𝑧))) |
96 | 95 | fveq1d 6771 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd ‘𝑃)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓)) = ((1st ↾ (𝑥(Hom ‘𝑇)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓))) |
97 | 84 | fvresd 6789 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥) = (1st ‘𝑥)) |
98 | 85 | fvresd 6789 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦) = (1st ‘𝑦)) |
99 | 97, 98 | opeq12d 4818 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 〈((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥), ((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦)〉 = 〈(1st ‘𝑥), (1st ‘𝑦)〉) |
100 | 86 | fvresd 6789 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑧) = (1st ‘𝑧)) |
101 | 99, 100 | oveq12d 7287 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (〈((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥), ((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦)〉(comp‘𝐶)((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑧)) = (〈(1st ‘𝑥), (1st ‘𝑦)〉(comp‘𝐶)(1st ‘𝑧))) |
102 | 1, 4, 5, 93, 94, 8, 85, 86 | 1stf2 17906 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑦(2nd ‘𝑃)𝑧) = (1st ↾ (𝑦(Hom ‘𝑇)𝑧))) |
103 | 102 | fveq1d 6771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑦(2nd ‘𝑃)𝑧)‘𝑔) = ((1st ↾ (𝑦(Hom ‘𝑇)𝑧))‘𝑔)) |
104 | 88 | fvresd 6789 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾ (𝑦(Hom ‘𝑇)𝑧))‘𝑔) = (1st ‘𝑔)) |
105 | 103, 104 | eqtrd 2780 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑦(2nd ‘𝑃)𝑧)‘𝑔) = (1st ‘𝑔)) |
106 | 1, 4, 5, 93, 94, 8, 84, 85 | 1stf2 17906 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑥(2nd ‘𝑃)𝑦) = (1st ↾ (𝑥(Hom ‘𝑇)𝑦))) |
107 | 106 | fveq1d 6771 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd ‘𝑃)𝑦)‘𝑓) = ((1st ↾ (𝑥(Hom ‘𝑇)𝑦))‘𝑓)) |
108 | 87 | fvresd 6789 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾ (𝑥(Hom ‘𝑇)𝑦))‘𝑓) = (1st ‘𝑓)) |
109 | 107, 108 | eqtrd 2780 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd ‘𝑃)𝑦)‘𝑓) = (1st ‘𝑓)) |
110 | 101, 105,
109 | oveq123d 7290 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (((𝑦(2nd ‘𝑃)𝑧)‘𝑔)(〈((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥), ((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦)〉(comp‘𝐶)((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑧))((𝑥(2nd ‘𝑃)𝑦)‘𝑓)) = ((1st ‘𝑔)(〈(1st
‘𝑥), (1st
‘𝑦)〉(comp‘𝐶)(1st ‘𝑧))(1st ‘𝑓))) |
111 | 92, 96, 110 | 3eqtr4d 2790 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd ‘𝑃)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓)) = (((𝑦(2nd ‘𝑃)𝑧)‘𝑔)(〈((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥), ((1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦)〉(comp‘𝐶)((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑧))((𝑥(2nd ‘𝑃)𝑦)‘𝑓))) |
112 | 4, 2, 5, 23, 24, 25, 26, 27, 28, 6, 30, 37, 56, 82, 111 | isfuncd 17576 |
. . 3
⊢ (𝜑 → (1st ↾
((Base‘𝐶) ×
(Base‘𝐷)))(𝑇 Func 𝐶)(2nd ‘𝑃)) |
113 | | df-br 5080 |
. . 3
⊢
((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))(𝑇 Func 𝐶)(2nd ‘𝑃) ↔ 〈(1st ↾
((Base‘𝐶) ×
(Base‘𝐷))),
(2nd ‘𝑃)〉 ∈ (𝑇 Func 𝐶)) |
114 | 112, 113 | sylib 217 |
. 2
⊢ (𝜑 → 〈(1st
↾ ((Base‘𝐶)
× (Base‘𝐷))),
(2nd ‘𝑃)〉 ∈ (𝑇 Func 𝐶)) |
115 | 22, 114 | eqeltrd 2841 |
1
⊢ (𝜑 → 𝑃 ∈ (𝑇 Func 𝐶)) |