| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1stfcl.t | . . . 4
⊢ 𝑇 = (𝐶 ×c 𝐷) | 
| 2 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝐶) =
(Base‘𝐶) | 
| 3 |  | eqid 2736 | . . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) | 
| 4 | 1, 2, 3 | xpcbas 18224 | . . . 4
⊢
((Base‘𝐶)
× (Base‘𝐷)) =
(Base‘𝑇) | 
| 5 |  | eqid 2736 | . . . 4
⊢ (Hom
‘𝑇) = (Hom
‘𝑇) | 
| 6 |  | 1stfcl.c | . . . 4
⊢ (𝜑 → 𝐶 ∈ Cat) | 
| 7 |  | 1stfcl.d | . . . 4
⊢ (𝜑 → 𝐷 ∈ Cat) | 
| 8 |  | 2ndfcl.p | . . . 4
⊢ 𝑄 = (𝐶 2ndF 𝐷) | 
| 9 | 1, 4, 5, 6, 7, 8 | 2ndfval 18240 | . . 3
⊢ (𝜑 → 𝑄 = 〈(2nd ↾
((Base‘𝐶) ×
(Base‘𝐷))), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (2nd ↾ (𝑥(Hom ‘𝑇)𝑦)))〉) | 
| 10 |  | fo2nd 8036 | . . . . . . . 8
⊢
2nd :V–onto→V | 
| 11 |  | fofun 6820 | . . . . . . . 8
⊢
(2nd :V–onto→V → Fun 2nd ) | 
| 12 | 10, 11 | ax-mp 5 | . . . . . . 7
⊢ Fun
2nd | 
| 13 |  | fvex 6918 | . . . . . . . 8
⊢
(Base‘𝐶)
∈ V | 
| 14 |  | fvex 6918 | . . . . . . . 8
⊢
(Base‘𝐷)
∈ V | 
| 15 | 13, 14 | xpex 7774 | . . . . . . 7
⊢
((Base‘𝐶)
× (Base‘𝐷))
∈ V | 
| 16 |  | resfunexg 7236 | . . . . . . 7
⊢ ((Fun
2nd ∧ ((Base‘𝐶) × (Base‘𝐷)) ∈ V) → (2nd ↾
((Base‘𝐶) ×
(Base‘𝐷))) ∈
V) | 
| 17 | 12, 15, 16 | mp2an 692 | . . . . . 6
⊢
(2nd ↾ ((Base‘𝐶) × (Base‘𝐷))) ∈ V | 
| 18 | 15, 15 | mpoex 8105 | . . . . . 6
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (2nd ↾ (𝑥(Hom ‘𝑇)𝑦))) ∈ V | 
| 19 | 17, 18 | op2ndd 8026 | . . . . 5
⊢ (𝑄 = 〈(2nd ↾
((Base‘𝐶) ×
(Base‘𝐷))), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (2nd ↾ (𝑥(Hom ‘𝑇)𝑦)))〉 → (2nd ‘𝑄) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (2nd ↾ (𝑥(Hom ‘𝑇)𝑦)))) | 
| 20 | 9, 19 | syl 17 | . . . 4
⊢ (𝜑 → (2nd
‘𝑄) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (2nd ↾ (𝑥(Hom ‘𝑇)𝑦)))) | 
| 21 | 20 | opeq2d 4879 | . . 3
⊢ (𝜑 → 〈(2nd
↾ ((Base‘𝐶)
× (Base‘𝐷))),
(2nd ‘𝑄)〉 = 〈(2nd ↾
((Base‘𝐶) ×
(Base‘𝐷))), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (2nd ↾ (𝑥(Hom ‘𝑇)𝑦)))〉) | 
| 22 | 9, 21 | eqtr4d 2779 | . 2
⊢ (𝜑 → 𝑄 = 〈(2nd ↾
((Base‘𝐶) ×
(Base‘𝐷))),
(2nd ‘𝑄)〉) | 
| 23 |  | eqid 2736 | . . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) | 
| 24 |  | eqid 2736 | . . . 4
⊢
(Id‘𝑇) =
(Id‘𝑇) | 
| 25 |  | eqid 2736 | . . . 4
⊢
(Id‘𝐷) =
(Id‘𝐷) | 
| 26 |  | eqid 2736 | . . . 4
⊢
(comp‘𝑇) =
(comp‘𝑇) | 
| 27 |  | eqid 2736 | . . . 4
⊢
(comp‘𝐷) =
(comp‘𝐷) | 
| 28 | 1, 6, 7 | xpccat 18236 | . . . 4
⊢ (𝜑 → 𝑇 ∈ Cat) | 
| 29 |  | f2ndres 8040 | . . . . 5
⊢
(2nd ↾ ((Base‘𝐶) × (Base‘𝐷))):((Base‘𝐶) × (Base‘𝐷))⟶(Base‘𝐷) | 
| 30 | 29 | a1i 11 | . . . 4
⊢ (𝜑 → (2nd ↾
((Base‘𝐶) ×
(Base‘𝐷))):((Base‘𝐶) × (Base‘𝐷))⟶(Base‘𝐷)) | 
| 31 |  | eqid 2736 | . . . . . 6
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (2nd ↾ (𝑥(Hom ‘𝑇)𝑦))) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (2nd ↾ (𝑥(Hom ‘𝑇)𝑦))) | 
| 32 |  | ovex 7465 | . . . . . . 7
⊢ (𝑥(Hom ‘𝑇)𝑦) ∈ V | 
| 33 |  | resfunexg 7236 | . . . . . . 7
⊢ ((Fun
2nd ∧ (𝑥(Hom
‘𝑇)𝑦) ∈ V) → (2nd ↾
(𝑥(Hom ‘𝑇)𝑦)) ∈ V) | 
| 34 | 12, 32, 33 | mp2an 692 | . . . . . 6
⊢
(2nd ↾ (𝑥(Hom ‘𝑇)𝑦)) ∈ V | 
| 35 | 31, 34 | fnmpoi 8096 | . . . . 5
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (2nd ↾ (𝑥(Hom ‘𝑇)𝑦))) Fn (((Base‘𝐶) × (Base‘𝐷)) × ((Base‘𝐶) × (Base‘𝐷))) | 
| 36 | 20 | fneq1d 6660 | . . . . 5
⊢ (𝜑 → ((2nd
‘𝑄) Fn
(((Base‘𝐶) ×
(Base‘𝐷)) ×
((Base‘𝐶) ×
(Base‘𝐷))) ↔
(𝑥 ∈
((Base‘𝐶) ×
(Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (2nd
↾ (𝑥(Hom ‘𝑇)𝑦))) Fn (((Base‘𝐶) × (Base‘𝐷)) × ((Base‘𝐶) × (Base‘𝐷))))) | 
| 37 | 35, 36 | mpbiri 258 | . . . 4
⊢ (𝜑 → (2nd
‘𝑄) Fn
(((Base‘𝐶) ×
(Base‘𝐷)) ×
((Base‘𝐶) ×
(Base‘𝐷)))) | 
| 38 |  | f2ndres 8040 | . . . . . 6
⊢
(2nd ↾ (((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))):(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))⟶((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)) | 
| 39 | 6 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → 𝐶 ∈ Cat) | 
| 40 | 7 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → 𝐷 ∈ Cat) | 
| 41 |  | simprl 770 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) | 
| 42 |  | simprr 772 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷))) | 
| 43 | 1, 4, 5, 39, 40, 8, 41, 42 | 2ndf2 18242 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd ‘𝑄)𝑦) = (2nd ↾ (𝑥(Hom ‘𝑇)𝑦))) | 
| 44 |  | eqid 2736 | . . . . . . . . . 10
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 45 | 1, 4, 44, 23, 5, 41, 42 | xpchom 18226 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(Hom ‘𝑇)𝑦) = (((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))) | 
| 46 | 45 | reseq2d 5996 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (2nd ↾ (𝑥(Hom ‘𝑇)𝑦)) = (2nd ↾
(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦))))) | 
| 47 | 43, 46 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd ‘𝑄)𝑦) = (2nd ↾ (((1st
‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd
‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦))))) | 
| 48 | 47 | feq1d 6719 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → ((𝑥(2nd ‘𝑄)𝑦):(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))⟶((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)) ↔ (2nd ↾
(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))):(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))⟶((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))) | 
| 49 | 38, 48 | mpbiri 258 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd ‘𝑄)𝑦):(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))⟶((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦))) | 
| 50 |  | fvres 6924 | . . . . . . . 8
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → ((2nd
↾ ((Base‘𝐶)
× (Base‘𝐷)))‘𝑥) = (2nd ‘𝑥)) | 
| 51 | 50 | ad2antrl 728 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → ((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥) = (2nd ‘𝑥)) | 
| 52 |  | fvres 6924 | . . . . . . . 8
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) → ((2nd
↾ ((Base‘𝐶)
× (Base‘𝐷)))‘𝑦) = (2nd ‘𝑦)) | 
| 53 | 52 | ad2antll 729 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → ((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦) = (2nd ‘𝑦)) | 
| 54 | 51, 53 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥)(Hom ‘𝐷)((2nd ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦)) = ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦))) | 
| 55 | 45, 54 | feq23d 6730 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → ((𝑥(2nd ‘𝑄)𝑦):(𝑥(Hom ‘𝑇)𝑦)⟶(((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥)(Hom ‘𝐷)((2nd ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦)) ↔ (𝑥(2nd ‘𝑄)𝑦):(((1st ‘𝑥)(Hom ‘𝐶)(1st ‘𝑦)) × ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))⟶((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)))) | 
| 56 | 49, 55 | mpbird 257 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd ‘𝑄)𝑦):(𝑥(Hom ‘𝑇)𝑦)⟶(((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥)(Hom ‘𝐷)((2nd ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦))) | 
| 57 | 28 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝑇 ∈ Cat) | 
| 58 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) | 
| 59 | 4, 5, 24, 57, 58 | catidcl 17726 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘𝑥) ∈ (𝑥(Hom ‘𝑇)𝑥)) | 
| 60 | 59 | fvresd 6925 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((2nd ↾ (𝑥(Hom ‘𝑇)𝑥))‘((Id‘𝑇)‘𝑥)) = (2nd ‘((Id‘𝑇)‘𝑥))) | 
| 61 |  | 1st2nd2 8054 | . . . . . . . . . 10
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 62 | 61 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) | 
| 63 | 62 | fveq2d 6909 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘𝑥) = ((Id‘𝑇)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) | 
| 64 | 6 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝐶 ∈ Cat) | 
| 65 | 7 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝐷 ∈ Cat) | 
| 66 |  | eqid 2736 | . . . . . . . . 9
⊢
(Id‘𝐶) =
(Id‘𝐶) | 
| 67 |  | xp1st 8047 | . . . . . . . . . 10
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → (1st
‘𝑥) ∈
(Base‘𝐶)) | 
| 68 | 67 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (1st ‘𝑥) ∈ (Base‘𝐶)) | 
| 69 |  | xp2nd 8048 | . . . . . . . . . 10
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → (2nd
‘𝑥) ∈
(Base‘𝐷)) | 
| 70 | 69 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (2nd ‘𝑥) ∈ (Base‘𝐷)) | 
| 71 | 1, 64, 65, 2, 3, 66, 25, 24, 68, 70 | xpcid 18235 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) =
〈((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐷)‘(2nd ‘𝑥))〉) | 
| 72 | 63, 71 | eqtrd 2776 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘𝑥) = 〈((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐷)‘(2nd ‘𝑥))〉) | 
| 73 |  | fvex 6918 | . . . . . . . 8
⊢
((Id‘𝐶)‘(1st ‘𝑥)) ∈ V | 
| 74 |  | fvex 6918 | . . . . . . . 8
⊢
((Id‘𝐷)‘(2nd ‘𝑥)) ∈ V | 
| 75 | 73, 74 | op2ndd 8026 | . . . . . . 7
⊢
(((Id‘𝑇)‘𝑥) = 〈((Id‘𝐶)‘(1st ‘𝑥)), ((Id‘𝐷)‘(2nd ‘𝑥))〉 → (2nd
‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐷)‘(2nd ‘𝑥))) | 
| 76 | 72, 75 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (2nd
‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐷)‘(2nd ‘𝑥))) | 
| 77 | 60, 76 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((2nd ↾ (𝑥(Hom ‘𝑇)𝑥))‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐷)‘(2nd ‘𝑥))) | 
| 78 | 1, 4, 5, 64, 65, 8, 58, 58 | 2ndf2 18242 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (𝑥(2nd ‘𝑄)𝑥) = (2nd ↾ (𝑥(Hom ‘𝑇)𝑥))) | 
| 79 | 78 | fveq1d 6907 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((𝑥(2nd ‘𝑄)𝑥)‘((Id‘𝑇)‘𝑥)) = ((2nd ↾ (𝑥(Hom ‘𝑇)𝑥))‘((Id‘𝑇)‘𝑥))) | 
| 80 | 50 | adantl 481 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥) = (2nd ‘𝑥)) | 
| 81 | 80 | fveq2d 6909 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝐷)‘((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥)) = ((Id‘𝐷)‘(2nd ‘𝑥))) | 
| 82 | 77, 79, 81 | 3eqtr4d 2786 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((𝑥(2nd ‘𝑄)𝑥)‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐷)‘((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥))) | 
| 83 | 28 | 3ad2ant1 1133 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑇 ∈ Cat) | 
| 84 |  | simp21 1206 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) | 
| 85 |  | simp22 1207 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷))) | 
| 86 |  | simp23 1208 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) | 
| 87 |  | simp3l 1201 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦)) | 
| 88 |  | simp3r 1202 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧)) | 
| 89 | 4, 5, 26, 83, 84, 85, 86, 87, 88 | catcocl 17729 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓) ∈ (𝑥(Hom ‘𝑇)𝑧)) | 
| 90 | 89 | fvresd 6925 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((2nd ↾ (𝑥(Hom ‘𝑇)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓)) = (2nd ‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓))) | 
| 91 | 1, 4, 5, 26, 84, 85, 86, 87, 88, 27 | xpcco2nd 18231 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (2nd ‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓)) = ((2nd ‘𝑔)(〈(2nd
‘𝑥), (2nd
‘𝑦)〉(comp‘𝐷)(2nd ‘𝑧))(2nd ‘𝑓))) | 
| 92 | 90, 91 | eqtrd 2776 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((2nd ↾ (𝑥(Hom ‘𝑇)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓)) = ((2nd ‘𝑔)(〈(2nd
‘𝑥), (2nd
‘𝑦)〉(comp‘𝐷)(2nd ‘𝑧))(2nd ‘𝑓))) | 
| 93 | 6 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝐶 ∈ Cat) | 
| 94 | 7 | 3ad2ant1 1133 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝐷 ∈ Cat) | 
| 95 | 1, 4, 5, 93, 94, 8, 84, 86 | 2ndf2 18242 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑥(2nd ‘𝑄)𝑧) = (2nd ↾ (𝑥(Hom ‘𝑇)𝑧))) | 
| 96 | 95 | fveq1d 6907 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd ‘𝑄)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓)) = ((2nd ↾ (𝑥(Hom ‘𝑇)𝑧))‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓))) | 
| 97 | 84 | fvresd 6925 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥) = (2nd ‘𝑥)) | 
| 98 | 85 | fvresd 6925 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦) = (2nd ‘𝑦)) | 
| 99 | 97, 98 | opeq12d 4880 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 〈((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥), ((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦)〉 = 〈(2nd ‘𝑥), (2nd ‘𝑦)〉) | 
| 100 | 86 | fvresd 6925 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑧) = (2nd ‘𝑧)) | 
| 101 | 99, 100 | oveq12d 7450 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (〈((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥), ((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦)〉(comp‘𝐷)((2nd ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑧)) = (〈(2nd ‘𝑥), (2nd ‘𝑦)〉(comp‘𝐷)(2nd ‘𝑧))) | 
| 102 | 1, 4, 5, 93, 94, 8, 85, 86 | 2ndf2 18242 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑦(2nd ‘𝑄)𝑧) = (2nd ↾ (𝑦(Hom ‘𝑇)𝑧))) | 
| 103 | 102 | fveq1d 6907 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑦(2nd ‘𝑄)𝑧)‘𝑔) = ((2nd ↾ (𝑦(Hom ‘𝑇)𝑧))‘𝑔)) | 
| 104 | 88 | fvresd 6925 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((2nd ↾ (𝑦(Hom ‘𝑇)𝑧))‘𝑔) = (2nd ‘𝑔)) | 
| 105 | 103, 104 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑦(2nd ‘𝑄)𝑧)‘𝑔) = (2nd ‘𝑔)) | 
| 106 | 1, 4, 5, 93, 94, 8, 84, 85 | 2ndf2 18242 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑥(2nd ‘𝑄)𝑦) = (2nd ↾ (𝑥(Hom ‘𝑇)𝑦))) | 
| 107 | 106 | fveq1d 6907 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd ‘𝑄)𝑦)‘𝑓) = ((2nd ↾ (𝑥(Hom ‘𝑇)𝑦))‘𝑓)) | 
| 108 | 87 | fvresd 6925 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((2nd ↾ (𝑥(Hom ‘𝑇)𝑦))‘𝑓) = (2nd ‘𝑓)) | 
| 109 | 107, 108 | eqtrd 2776 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd ‘𝑄)𝑦)‘𝑓) = (2nd ‘𝑓)) | 
| 110 | 101, 105,
109 | oveq123d 7453 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (((𝑦(2nd ‘𝑄)𝑧)‘𝑔)(〈((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥), ((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦)〉(comp‘𝐷)((2nd ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑧))((𝑥(2nd ‘𝑄)𝑦)‘𝑓)) = ((2nd ‘𝑔)(〈(2nd
‘𝑥), (2nd
‘𝑦)〉(comp‘𝐷)(2nd ‘𝑧))(2nd ‘𝑓))) | 
| 111 | 92, 96, 110 | 3eqtr4d 2786 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd ‘𝑄)𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑇)𝑧)𝑓)) = (((𝑦(2nd ‘𝑄)𝑧)‘𝑔)(〈((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑥), ((2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))‘𝑦)〉(comp‘𝐷)((2nd ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑧))((𝑥(2nd ‘𝑄)𝑦)‘𝑓))) | 
| 112 | 4, 3, 5, 23, 24, 25, 26, 27, 28, 7, 30, 37, 56, 82, 111 | isfuncd 17911 | . . 3
⊢ (𝜑 → (2nd ↾
((Base‘𝐶) ×
(Base‘𝐷)))(𝑇 Func 𝐷)(2nd ‘𝑄)) | 
| 113 |  | df-br 5143 | . . 3
⊢
((2nd ↾ ((Base‘𝐶) × (Base‘𝐷)))(𝑇 Func 𝐷)(2nd ‘𝑄) ↔ 〈(2nd ↾
((Base‘𝐶) ×
(Base‘𝐷))),
(2nd ‘𝑄)〉 ∈ (𝑇 Func 𝐷)) | 
| 114 | 112, 113 | sylib 218 | . 2
⊢ (𝜑 → 〈(2nd
↾ ((Base‘𝐶)
× (Base‘𝐷))),
(2nd ‘𝑄)〉 ∈ (𝑇 Func 𝐷)) | 
| 115 | 22, 114 | eqeltrd 2840 | 1
⊢ (𝜑 → 𝑄 ∈ (𝑇 Func 𝐷)) |