MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1stfcl Structured version   Visualization version   GIF version

Theorem 1stfcl 17449
Description: The first projection functor is a functor onto the left argument. (Contributed by Mario Carneiro, 11-Jan-2017.)
Hypotheses
Ref Expression
1stfcl.t 𝑇 = (𝐶 ×c 𝐷)
1stfcl.c (𝜑𝐶 ∈ Cat)
1stfcl.d (𝜑𝐷 ∈ Cat)
1stfcl.p 𝑃 = (𝐶 1stF 𝐷)
Assertion
Ref Expression
1stfcl (𝜑𝑃 ∈ (𝑇 Func 𝐶))

Proof of Theorem 1stfcl
Dummy variables 𝑓 𝑔 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1stfcl.t . . . 4 𝑇 = (𝐶 ×c 𝐷)
2 eqid 2824 . . . . 5 (Base‘𝐶) = (Base‘𝐶)
3 eqid 2824 . . . . 5 (Base‘𝐷) = (Base‘𝐷)
41, 2, 3xpcbas 17430 . . . 4 ((Base‘𝐶) × (Base‘𝐷)) = (Base‘𝑇)
5 eqid 2824 . . . 4 (Hom ‘𝑇) = (Hom ‘𝑇)
6 1stfcl.c . . . 4 (𝜑𝐶 ∈ Cat)
7 1stfcl.d . . . 4 (𝜑𝐷 ∈ Cat)
8 1stfcl.p . . . 4 𝑃 = (𝐶 1stF 𝐷)
91, 4, 5, 6, 7, 81stfval 17443 . . 3 (𝜑𝑃 = ⟨(1st ↾ ((Base‘𝐶) × (Base‘𝐷))), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦)))⟩)
10 fo1st 7706 . . . . . . . 8 1st :V–onto→V
11 fofun 6584 . . . . . . . 8 (1st :V–onto→V → Fun 1st )
1210, 11ax-mp 5 . . . . . . 7 Fun 1st
13 fvex 6676 . . . . . . . 8 (Base‘𝐶) ∈ V
14 fvex 6676 . . . . . . . 8 (Base‘𝐷) ∈ V
1513, 14xpex 7472 . . . . . . 7 ((Base‘𝐶) × (Base‘𝐷)) ∈ V
16 resfunexg 6971 . . . . . . 7 ((Fun 1st ∧ ((Base‘𝐶) × (Base‘𝐷)) ∈ V) → (1st ↾ ((Base‘𝐶) × (Base‘𝐷))) ∈ V)
1712, 15, 16mp2an 691 . . . . . 6 (1st ↾ ((Base‘𝐶) × (Base‘𝐷))) ∈ V
1815, 15mpoex 7775 . . . . . 6 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦))) ∈ V
1917, 18op2ndd 7697 . . . . 5 (𝑃 = ⟨(1st ↾ ((Base‘𝐶) × (Base‘𝐷))), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦)))⟩ → (2nd𝑃) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦))))
209, 19syl 17 . . . 4 (𝜑 → (2nd𝑃) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦))))
2120opeq2d 4796 . . 3 (𝜑 → ⟨(1st ↾ ((Base‘𝐶) × (Base‘𝐷))), (2nd𝑃)⟩ = ⟨(1st ↾ ((Base‘𝐶) × (Base‘𝐷))), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦)))⟩)
229, 21eqtr4d 2862 . 2 (𝜑𝑃 = ⟨(1st ↾ ((Base‘𝐶) × (Base‘𝐷))), (2nd𝑃)⟩)
23 eqid 2824 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
24 eqid 2824 . . . 4 (Id‘𝑇) = (Id‘𝑇)
25 eqid 2824 . . . 4 (Id‘𝐶) = (Id‘𝐶)
26 eqid 2824 . . . 4 (comp‘𝑇) = (comp‘𝑇)
27 eqid 2824 . . . 4 (comp‘𝐶) = (comp‘𝐶)
281, 6, 7xpccat 17442 . . . 4 (𝜑𝑇 ∈ Cat)
29 f1stres 7710 . . . . 5 (1st ↾ ((Base‘𝐶) × (Base‘𝐷))):((Base‘𝐶) × (Base‘𝐷))⟶(Base‘𝐶)
3029a1i 11 . . . 4 (𝜑 → (1st ↾ ((Base‘𝐶) × (Base‘𝐷))):((Base‘𝐶) × (Base‘𝐷))⟶(Base‘𝐶))
31 eqid 2824 . . . . . 6 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦))) = (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦)))
32 ovex 7184 . . . . . . 7 (𝑥(Hom ‘𝑇)𝑦) ∈ V
33 resfunexg 6971 . . . . . . 7 ((Fun 1st ∧ (𝑥(Hom ‘𝑇)𝑦) ∈ V) → (1st ↾ (𝑥(Hom ‘𝑇)𝑦)) ∈ V)
3412, 32, 33mp2an 691 . . . . . 6 (1st ↾ (𝑥(Hom ‘𝑇)𝑦)) ∈ V
3531, 34fnmpoi 7765 . . . . 5 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦))) Fn (((Base‘𝐶) × (Base‘𝐷)) × ((Base‘𝐶) × (Base‘𝐷)))
3620fneq1d 6436 . . . . 5 (𝜑 → ((2nd𝑃) Fn (((Base‘𝐶) × (Base‘𝐷)) × ((Base‘𝐶) × (Base‘𝐷))) ↔ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ↦ (1st ↾ (𝑥(Hom ‘𝑇)𝑦))) Fn (((Base‘𝐶) × (Base‘𝐷)) × ((Base‘𝐶) × (Base‘𝐷)))))
3735, 36mpbiri 261 . . . 4 (𝜑 → (2nd𝑃) Fn (((Base‘𝐶) × (Base‘𝐷)) × ((Base‘𝐶) × (Base‘𝐷))))
38 f1stres 7710 . . . . . 6 (1st ↾ (((1st𝑥)(Hom ‘𝐶)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐷)(2nd𝑦)))):(((1st𝑥)(Hom ‘𝐶)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐷)(2nd𝑦)))⟶((1st𝑥)(Hom ‘𝐶)(1st𝑦))
396adantr 484 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → 𝐶 ∈ Cat)
407adantr 484 . . . . . . . . 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‘𝐷)))
431, 4, 5, 39, 40, 8, 41, 421stf2 17445 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd𝑃)𝑦) = (1st ↾ (𝑥(Hom ‘𝑇)𝑦)))
44 eqid 2824 . . . . . . . . . 10 (Hom ‘𝐷) = (Hom ‘𝐷)
451, 4, 23, 44, 5, 41, 42xpchom 17432 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(Hom ‘𝑇)𝑦) = (((1st𝑥)(Hom ‘𝐶)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐷)(2nd𝑦))))
4645reseq2d 5842 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (1st ↾ (𝑥(Hom ‘𝑇)𝑦)) = (1st ↾ (((1st𝑥)(Hom ‘𝐶)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐷)(2nd𝑦)))))
4743, 46eqtrd 2859 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd𝑃)𝑦) = (1st ↾ (((1st𝑥)(Hom ‘𝐶)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐷)(2nd𝑦)))))
4847feq1d 6490 . . . . . 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𝑦))))
4938, 48mpbiri 261 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd𝑃)𝑦):(((1st𝑥)(Hom ‘𝐶)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐷)(2nd𝑦)))⟶((1st𝑥)(Hom ‘𝐶)(1st𝑦)))
50 fvres 6682 . . . . . . . 8 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥) = (1st𝑥))
5150ad2antrl 727 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥) = (1st𝑥))
52 fvres 6682 . . . . . . . 8 (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) → ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦) = (1st𝑦))
5352ad2antll 728 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦) = (1st𝑦))
5451, 53oveq12d 7169 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥)(Hom ‘𝐶)((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦)) = ((1st𝑥)(Hom ‘𝐶)(1st𝑦)))
5545, 54feq23d 6500 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → ((𝑥(2nd𝑃)𝑦):(𝑥(Hom ‘𝑇)𝑦)⟶(((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥)(Hom ‘𝐶)((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦)) ↔ (𝑥(2nd𝑃)𝑦):(((1st𝑥)(Hom ‘𝐶)(1st𝑦)) × ((2nd𝑥)(Hom ‘𝐷)(2nd𝑦)))⟶((1st𝑥)(Hom ‘𝐶)(1st𝑦))))
5649, 55mpbird 260 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))) → (𝑥(2nd𝑃)𝑦):(𝑥(Hom ‘𝑇)𝑦)⟶(((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥)(Hom ‘𝐶)((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦)))
5728adantr 484 . . . . . . . 8 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝑇 ∈ Cat)
58 simpr 488 . . . . . . . 8 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)))
594, 5, 24, 57, 58catidcl 16955 . . . . . . 7 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘𝑥) ∈ (𝑥(Hom ‘𝑇)𝑥))
6059fvresd 6683 . . . . . 6 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((1st ↾ (𝑥(Hom ‘𝑇)𝑥))‘((Id‘𝑇)‘𝑥)) = (1st ‘((Id‘𝑇)‘𝑥)))
61 1st2nd2 7725 . . . . . . . . . 10 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
6261adantl 485 . . . . . . . . 9 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝑥 = ⟨(1st𝑥), (2nd𝑥)⟩)
6362fveq2d 6667 . . . . . . . 8 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘𝑥) = ((Id‘𝑇)‘⟨(1st𝑥), (2nd𝑥)⟩))
646adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝐶 ∈ Cat)
657adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → 𝐷 ∈ Cat)
66 eqid 2824 . . . . . . . . 9 (Id‘𝐷) = (Id‘𝐷)
67 xp1st 7718 . . . . . . . . . 10 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → (1st𝑥) ∈ (Base‘𝐶))
6867adantl 485 . . . . . . . . 9 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (1st𝑥) ∈ (Base‘𝐶))
69 xp2nd 7719 . . . . . . . . . 10 (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) → (2nd𝑥) ∈ (Base‘𝐷))
7069adantl 485 . . . . . . . . 9 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (2nd𝑥) ∈ (Base‘𝐷))
711, 64, 65, 2, 3, 25, 66, 24, 68, 70xpcid 17441 . . . . . . . 8 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘⟨(1st𝑥), (2nd𝑥)⟩) = ⟨((Id‘𝐶)‘(1st𝑥)), ((Id‘𝐷)‘(2nd𝑥))⟩)
7263, 71eqtrd 2859 . . . . . . 7 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝑇)‘𝑥) = ⟨((Id‘𝐶)‘(1st𝑥)), ((Id‘𝐷)‘(2nd𝑥))⟩)
73 fvex 6676 . . . . . . . 8 ((Id‘𝐶)‘(1st𝑥)) ∈ V
74 fvex 6676 . . . . . . . 8 ((Id‘𝐷)‘(2nd𝑥)) ∈ V
7573, 74op1std 7696 . . . . . . 7 (((Id‘𝑇)‘𝑥) = ⟨((Id‘𝐶)‘(1st𝑥)), ((Id‘𝐷)‘(2nd𝑥))⟩ → (1st ‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐶)‘(1st𝑥)))
7672, 75syl 17 . . . . . 6 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (1st ‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐶)‘(1st𝑥)))
7760, 76eqtrd 2859 . . . . 5 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((1st ↾ (𝑥(Hom ‘𝑇)𝑥))‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐶)‘(1st𝑥)))
781, 4, 5, 64, 65, 8, 58, 581stf2 17445 . . . . . 6 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → (𝑥(2nd𝑃)𝑥) = (1st ↾ (𝑥(Hom ‘𝑇)𝑥)))
7978fveq1d 6665 . . . . 5 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((𝑥(2nd𝑃)𝑥)‘((Id‘𝑇)‘𝑥)) = ((1st ↾ (𝑥(Hom ‘𝑇)𝑥))‘((Id‘𝑇)‘𝑥)))
8050adantl 485 . . . . . 6 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥) = (1st𝑥))
8180fveq2d 6667 . . . . 5 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((Id‘𝐶)‘((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥)) = ((Id‘𝐶)‘(1st𝑥)))
8277, 79, 813eqtr4d 2869 . . . 4 ((𝜑𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷))) → ((𝑥(2nd𝑃)𝑥)‘((Id‘𝑇)‘𝑥)) = ((Id‘𝐶)‘((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥)))
83283ad2ant1 1130 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑇 ∈ Cat)
84 simp21 1203 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)))
85 simp22 1204 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)))
86 simp23 1205 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷)))
87 simp3l 1198 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦))
88 simp3r 1199 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))
894, 5, 26, 83, 84, 85, 86, 87, 88catcocl 16958 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑇)𝑧)𝑓) ∈ (𝑥(Hom ‘𝑇)𝑧))
9089fvresd 6683 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾ (𝑥(Hom ‘𝑇)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑇)𝑧)𝑓)) = (1st ‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑇)𝑧)𝑓)))
911, 4, 5, 26, 84, 85, 86, 87, 88, 27xpcco1st 17436 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (1st ‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑇)𝑧)𝑓)) = ((1st𝑔)(⟨(1st𝑥), (1st𝑦)⟩(comp‘𝐶)(1st𝑧))(1st𝑓)))
9290, 91eqtrd 2859 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾ (𝑥(Hom ‘𝑇)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑇)𝑧)𝑓)) = ((1st𝑔)(⟨(1st𝑥), (1st𝑦)⟩(comp‘𝐶)(1st𝑧))(1st𝑓)))
9363ad2ant1 1130 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝐶 ∈ Cat)
9473ad2ant1 1130 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → 𝐷 ∈ Cat)
951, 4, 5, 93, 94, 8, 84, 861stf2 17445 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑥(2nd𝑃)𝑧) = (1st ↾ (𝑥(Hom ‘𝑇)𝑧)))
9695fveq1d 6665 . . . . 5 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd𝑃)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑇)𝑧)𝑓)) = ((1st ↾ (𝑥(Hom ‘𝑇)𝑧))‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑇)𝑧)𝑓)))
9784fvresd 6683 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥) = (1st𝑥))
9885fvresd 6683 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦) = (1st𝑦))
9997, 98opeq12d 4797 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ⟨((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥), ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦)⟩ = ⟨(1st𝑥), (1st𝑦)⟩)
10086fvresd 6683 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑧) = (1st𝑧))
10199, 100oveq12d 7169 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (⟨((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥), ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦)⟩(comp‘𝐶)((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑧)) = (⟨(1st𝑥), (1st𝑦)⟩(comp‘𝐶)(1st𝑧)))
1021, 4, 5, 93, 94, 8, 85, 861stf2 17445 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑦(2nd𝑃)𝑧) = (1st ↾ (𝑦(Hom ‘𝑇)𝑧)))
103102fveq1d 6665 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑦(2nd𝑃)𝑧)‘𝑔) = ((1st ↾ (𝑦(Hom ‘𝑇)𝑧))‘𝑔))
10488fvresd 6683 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾ (𝑦(Hom ‘𝑇)𝑧))‘𝑔) = (1st𝑔))
105103, 104eqtrd 2859 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑦(2nd𝑃)𝑧)‘𝑔) = (1st𝑔))
1061, 4, 5, 93, 94, 8, 84, 851stf2 17445 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → (𝑥(2nd𝑃)𝑦) = (1st ↾ (𝑥(Hom ‘𝑇)𝑦)))
107106fveq1d 6665 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd𝑃)𝑦)‘𝑓) = ((1st ↾ (𝑥(Hom ‘𝑇)𝑦))‘𝑓))
10887fvresd 6683 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((1st ↾ (𝑥(Hom ‘𝑇)𝑦))‘𝑓) = (1st𝑓))
109107, 108eqtrd 2859 . . . . . 6 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd𝑃)𝑦)‘𝑓) = (1st𝑓))
110101, 105, 109oveq123d 7172 . . . . 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𝑓)))
11192, 96, 1103eqtr4d 2869 . . . 4 ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐷)) ∧ 𝑧 ∈ ((Base‘𝐶) × (Base‘𝐷))) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑇)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑇)𝑧))) → ((𝑥(2nd𝑃)𝑧)‘(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑇)𝑧)𝑓)) = (((𝑦(2nd𝑃)𝑧)‘𝑔)(⟨((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑥), ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑦)⟩(comp‘𝐶)((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))‘𝑧))((𝑥(2nd𝑃)𝑦)‘𝑓)))
1124, 2, 5, 23, 24, 25, 26, 27, 28, 6, 30, 37, 56, 82, 111isfuncd 17137 . . 3 (𝜑 → (1st ↾ ((Base‘𝐶) × (Base‘𝐷)))(𝑇 Func 𝐶)(2nd𝑃))
113 df-br 5054 . . 3 ((1st ↾ ((Base‘𝐶) × (Base‘𝐷)))(𝑇 Func 𝐶)(2nd𝑃) ↔ ⟨(1st ↾ ((Base‘𝐶) × (Base‘𝐷))), (2nd𝑃)⟩ ∈ (𝑇 Func 𝐶))
114112, 113sylib 221 . 2 (𝜑 → ⟨(1st ↾ ((Base‘𝐶) × (Base‘𝐷))), (2nd𝑃)⟩ ∈ (𝑇 Func 𝐶))
11522, 114eqeltrd 2916 1 (𝜑𝑃 ∈ (𝑇 Func 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2115  Vcvv 3480  cop 4556   class class class wbr 5053   × cxp 5541  cres 5545  Fun wfun 6339   Fn wfn 6340  wf 6341  ontowfo 6343  cfv 6345  (class class class)co 7151  cmpo 7153  1st c1st 7684  2nd c2nd 7685  Basecbs 16485  Hom chom 16578  compcco 16579  Catccat 16937  Idccid 16938   Func cfunc 17126   ×c cxpc 17420   1stF c1stf 17421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5177  ax-sep 5190  ax-nul 5197  ax-pow 5254  ax-pr 5318  ax-un 7457  ax-cnex 10593  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-br 5054  df-opab 5116  df-mpt 5134  df-tr 5160  df-id 5448  df-eprel 5453  df-po 5462  df-so 5463  df-fr 5502  df-we 5504  df-xp 5549  df-rel 5550  df-cnv 5551  df-co 5552  df-dm 5553  df-rn 5554  df-res 5555  df-ima 5556  df-pred 6137  df-ord 6183  df-on 6184  df-lim 6185  df-suc 6186  df-iota 6304  df-fun 6347  df-fn 6348  df-f 6349  df-f1 6350  df-fo 6351  df-f1o 6352  df-fv 6353  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7577  df-1st 7686  df-2nd 7687  df-wrecs 7945  df-recs 8006  df-rdg 8044  df-1o 8100  df-oadd 8104  df-er 8287  df-map 8406  df-ixp 8460  df-en 8508  df-dom 8509  df-sdom 8510  df-fin 8511  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-nn 11637  df-2 11699  df-3 11700  df-4 11701  df-5 11702  df-6 11703  df-7 11704  df-8 11705  df-9 11706  df-n0 11897  df-z 11981  df-dec 12098  df-uz 12243  df-fz 12897  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-hom 16591  df-cco 16592  df-cat 16941  df-cid 16942  df-func 17130  df-xpc 17424  df-1stf 17425
This theorem is referenced by:  prf1st  17456  1st2ndprf  17458  uncfcl  17487  uncf1  17488  uncf2  17489  diagcl  17493  diag11  17495  diag12  17496  diag2  17497  yonedalem1  17524  yonedalem21  17525  yonedalem22  17530
  Copyright terms: Public domain W3C validator