1stfcl

Description: The first projection functor is a functor onto the left argument. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	1stfcl.t	$⊢ T = C \times_{c} D$
	1stfcl.c	$⊢ φ \to C \in Cat$
	1stfcl.d	$⊢ φ \to D \in Cat$
	1stfcl.p	$⊢ P = C {1^{st}}_{F} D$
Assertion	1stfcl	$⊢ φ \to P \in (T Func C)$

Proof

Step	Hyp	Ref	Expression
1		1stfcl.t	$⊢ T = C \times_{c} D$
2		1stfcl.c	$⊢ φ \to C \in Cat$
3		1stfcl.d	$⊢ φ \to D \in Cat$
4		1stfcl.p	$⊢ P = C {1^{st}}_{F} D$
5		eqid	$⊢ {Base}_{C} = {Base}_{C}$
6		eqid	$⊢ {Base}_{D} = {Base}_{D}$
7	1 5 6	xpcbas	$⊢ {Base}_{C} \times {Base}_{D} = {Base}_{T}$
8		eqid	$⊢ Hom (T) = Hom (T)$
9	1 7 8 2 3 4	1stfval	$⊢ φ \to P = ⟨{1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}, (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (T) y)})⟩$
10		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
11		fofun	$⊢ 1^{st} : V \underset{onto}{⟶} V \to Fun 1^{st}$
12	10 11	ax-mp	$⊢ Fun 1^{st}$
13		fvex	$⊢ {Base}_{C} \in V$
14		fvex	$⊢ {Base}_{D} \in V$
15	13 14	xpex	$⊢ {Base}_{C} \times {Base}_{D} \in V$
16		resfunexg	$⊢ (Fun 1^{st} \land {Base}_{C} \times {Base}_{D} \in V) \to {1^{st} ↾}_{({Base}_{C} \times {Base}_{D})} \in V$
17	12 15 16	mp2an	$⊢ {1^{st} ↾}_{({Base}_{C} \times {Base}_{D})} \in V$
18	15 15	mpoex	$⊢ (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (T) y)}) \in V$
19	17 18	op2ndd	$⊢ P = ⟨{1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}, (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (T) y)})⟩ \to 2^{nd} (P) = (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (T) y)})$
20	9 19	syl	$⊢ φ \to 2^{nd} (P) = (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (T) y)})$
21	20	opeq2d	$⊢ φ \to ⟨{1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}, 2^{nd} (P)⟩ = ⟨{1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}, (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (T) y)})⟩$
22	9 21	eqtr4d	$⊢ φ \to P = ⟨{1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}, 2^{nd} (P)⟩$
23		eqid	$⊢ Hom (C) = Hom (C)$
24		eqid	$⊢ Id (T) = Id (T)$
25		eqid	$⊢ Id (C) = Id (C)$
26		eqid	$⊢ comp (T) = comp (T)$
27		eqid	$⊢ comp (C) = comp (C)$
28	1 2 3	xpccat	$⊢ φ \to T \in Cat$
29		f1stres	$⊢ ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) : {Base}_{C} \times {Base}_{D} ⟶ {Base}_{C}$
30	29	a1i	$⊢ φ \to ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) : {Base}_{C} \times {Base}_{D} ⟶ {Base}_{C}$
31		eqid	$⊢ (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (T) y)}) = (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (T) y)})$
32		ovex	$⊢ x Hom (T) y \in V$
33		resfunexg	$⊢ (Fun 1^{st} \land x Hom (T) y \in V) \to {1^{st} ↾}_{(x Hom (T) y)} \in V$
34	12 32 33	mp2an	$⊢ {1^{st} ↾}_{(x Hom (T) y)} \in V$
35	31 34	fnmpoi	$⊢ (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (T) y)}) Fn (({Base}_{C} \times {Base}_{D}) \times ({Base}_{C} \times {Base}_{D}))$
36	20	fneq1d	$⊢ φ \to (2^{nd} (P) Fn (({Base}_{C} \times {Base}_{D}) \times ({Base}_{C} \times {Base}_{D})) \leftrightarrow (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (T) y)}) Fn (({Base}_{C} \times {Base}_{D}) \times ({Base}_{C} \times {Base}_{D})))$
37	35 36	mpbiri	$⊢ φ \to 2^{nd} (P) Fn (({Base}_{C} \times {Base}_{D}) \times ({Base}_{C} \times {Base}_{D}))$
38		f1stres	$⊢ ({1^{st} ↾}_{((1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)))}) : (1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟶ 1^{st} (x) Hom (C) 1^{st} (y)$
39	2	adantr	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to C \in Cat$
40	3	adantr	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to D \in Cat$
41		simprl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to x \in ({Base}_{C} \times {Base}_{D})$
42		simprr	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to y \in ({Base}_{C} \times {Base}_{D})$
43	1 7 8 39 40 4 41 42	1stf2	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to x 2^{nd} (P) y = {1^{st} ↾}_{(x Hom (T) y)}$
44		eqid	$⊢ Hom (D) = Hom (D)$
45	1 7 23 44 8 41 42	xpchom	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to x Hom (T) y = (1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y))$
46	45	reseq2d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to {1^{st} ↾}_{(x Hom (T) y)} = {1^{st} ↾}_{((1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)))}$
47	43 46	eqtrd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to x 2^{nd} (P) y = {1^{st} ↾}_{((1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)))}$
48	47	feq1d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to ((x 2^{nd} (P) y) : (1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟶ 1^{st} (x) Hom (C) 1^{st} (y) \leftrightarrow ({1^{st} ↾}_{((1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)))}) : (1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟶ 1^{st} (x) Hom (C) 1^{st} (y))$
49	38 48	mpbiri	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to (x 2^{nd} (P) y) : (1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟶ 1^{st} (x) Hom (C) 1^{st} (y)$
50		fvres	$⊢ x \in ({Base}_{C} \times {Base}_{D}) \to ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) = 1^{st} (x)$
51	50	ad2antrl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) = 1^{st} (x)$
52		fvres	$⊢ y \in ({Base}_{C} \times {Base}_{D}) \to ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (y) = 1^{st} (y)$
53	52	ad2antll	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (y) = 1^{st} (y)$
54	51 53	oveq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) Hom (C) ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (y) = 1^{st} (x) Hom (C) 1^{st} (y)$
55	45 54	feq23d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to ((x 2^{nd} (P) y) : x Hom (T) y ⟶ ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) Hom (C) ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (y) \leftrightarrow (x 2^{nd} (P) y) : (1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟶ 1^{st} (x) Hom (C) 1^{st} (y))$
56	49 55	mpbird	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to (x 2^{nd} (P) y) : x Hom (T) y ⟶ ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) Hom (C) ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (y)$
57	28	adantr	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to T \in Cat$
58		simpr	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to x \in ({Base}_{C} \times {Base}_{D})$
59	7 8 24 57 58	catidcl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to Id (T) (x) \in (x Hom (T) x)$
60	59	fvresd	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to ({1^{st} ↾}_{(x Hom (T) x)}) (Id (T) (x)) = 1^{st} (Id (T) (x))$
61		1st2nd2	$⊢ x \in ({Base}_{C} \times {Base}_{D}) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
62	61	adantl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to x = ⟨1^{st} (x), 2^{nd} (x)⟩$
63	62	fveq2d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to Id (T) (x) = Id (T) (⟨1^{st} (x), 2^{nd} (x)⟩)$
64	2	adantr	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to C \in Cat$
65	3	adantr	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to D \in Cat$
66		eqid	$⊢ Id (D) = Id (D)$
67		xp1st	$⊢ x \in ({Base}_{C} \times {Base}_{D}) \to 1^{st} (x) \in {Base}_{C}$
68	67	adantl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to 1^{st} (x) \in {Base}_{C}$
69		xp2nd	$⊢ x \in ({Base}_{C} \times {Base}_{D}) \to 2^{nd} (x) \in {Base}_{D}$
70	69	adantl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to 2^{nd} (x) \in {Base}_{D}$
71	1 64 65 5 6 25 66 24 68 70	xpcid	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to Id (T) (⟨1^{st} (x), 2^{nd} (x)⟩) = ⟨Id (C) (1^{st} (x)), Id (D) (2^{nd} (x))⟩$
72	63 71	eqtrd	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to Id (T) (x) = ⟨Id (C) (1^{st} (x)), Id (D) (2^{nd} (x))⟩$
73		fvex	$⊢ Id (C) (1^{st} (x)) \in V$
74		fvex	$⊢ Id (D) (2^{nd} (x)) \in V$
75	73 74	op1std	$⊢ Id (T) (x) = ⟨Id (C) (1^{st} (x)), Id (D) (2^{nd} (x))⟩ \to 1^{st} (Id (T) (x)) = Id (C) (1^{st} (x))$
76	72 75	syl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to 1^{st} (Id (T) (x)) = Id (C) (1^{st} (x))$
77	60 76	eqtrd	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to ({1^{st} ↾}_{(x Hom (T) x)}) (Id (T) (x)) = Id (C) (1^{st} (x))$
78	1 7 8 64 65 4 58 58	1stf2	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to x 2^{nd} (P) x = {1^{st} ↾}_{(x Hom (T) x)}$
79	78	fveq1d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to (x 2^{nd} (P) x) (Id (T) (x)) = ({1^{st} ↾}_{(x Hom (T) x)}) (Id (T) (x))$
80	50	adantl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) = 1^{st} (x)$
81	80	fveq2d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to Id (C) (({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x)) = Id (C) (1^{st} (x))$
82	77 79 81	3eqtr4d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to (x 2^{nd} (P) x) (Id (T) (x)) = Id (C) (({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x))$
83	28	3ad2ant1	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to T \in Cat$
84		simp21	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to x \in ({Base}_{C} \times {Base}_{D})$
85		simp22	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to y \in ({Base}_{C} \times {Base}_{D})$
86		simp23	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to z \in ({Base}_{C} \times {Base}_{D})$
87		simp3l	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to f \in (x Hom (T) y)$
88		simp3r	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to g \in (y Hom (T) z)$
89	7 8 26 83 84 85 86 87 88	catcocl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to g (⟨x, y⟩ comp (T) z) f \in (x Hom (T) z)$
90	89	fvresd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to ({1^{st} ↾}_{(x Hom (T) z)}) (g (⟨x, y⟩ comp (T) z) f) = 1^{st} (g (⟨x, y⟩ comp (T) z) f)$
91	1 7 8 26 84 85 86 87 88 27	xpcco1st	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to 1^{st} (g (⟨x, y⟩ comp (T) z) f) = 1^{st} (g) (⟨1^{st} (x), 1^{st} (y)⟩ comp (C) 1^{st} (z)) 1^{st} (f)$
92	90 91	eqtrd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to ({1^{st} ↾}_{(x Hom (T) z)}) (g (⟨x, y⟩ comp (T) z) f) = 1^{st} (g) (⟨1^{st} (x), 1^{st} (y)⟩ comp (C) 1^{st} (z)) 1^{st} (f)$
93	2	3ad2ant1	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to C \in Cat$
94	3	3ad2ant1	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to D \in Cat$
95	1 7 8 93 94 4 84 86	1stf2	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to x 2^{nd} (P) z = {1^{st} ↾}_{(x Hom (T) z)}$
96	95	fveq1d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to (x 2^{nd} (P) z) (g (⟨x, y⟩ comp (T) z) f) = ({1^{st} ↾}_{(x Hom (T) z)}) (g (⟨x, y⟩ comp (T) z) f)$
97	84	fvresd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) = 1^{st} (x)$
98	85	fvresd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (y) = 1^{st} (y)$
99	97 98	opeq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to ⟨({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x), ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (y)⟩ = ⟨1^{st} (x), 1^{st} (y)⟩$
100	86	fvresd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (z) = 1^{st} (z)$
101	99 100	oveq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to ⟨({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x), ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (y)⟩ comp (C) ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (z) = ⟨1^{st} (x), 1^{st} (y)⟩ comp (C) 1^{st} (z)$
102	1 7 8 93 94 4 85 86	1stf2	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to y 2^{nd} (P) z = {1^{st} ↾}_{(y Hom (T) z)}$
103	102	fveq1d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to (y 2^{nd} (P) z) (g) = ({1^{st} ↾}_{(y Hom (T) z)}) (g)$
104	88	fvresd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to ({1^{st} ↾}_{(y Hom (T) z)}) (g) = 1^{st} (g)$
105	103 104	eqtrd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to (y 2^{nd} (P) z) (g) = 1^{st} (g)$
106	1 7 8 93 94 4 84 85	1stf2	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to x 2^{nd} (P) y = {1^{st} ↾}_{(x Hom (T) y)}$
107	106	fveq1d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to (x 2^{nd} (P) y) (f) = ({1^{st} ↾}_{(x Hom (T) y)}) (f)$
108	87	fvresd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to ({1^{st} ↾}_{(x Hom (T) y)}) (f) = 1^{st} (f)$
109	107 108	eqtrd	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to (x 2^{nd} (P) y) (f) = 1^{st} (f)$
110	101 105 109	oveq123d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to (y 2^{nd} (P) z) (g) (⟨({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x), ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (y)⟩ comp (C) ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (z)) (x 2^{nd} (P) y) (f) = 1^{st} (g) (⟨1^{st} (x), 1^{st} (y)⟩ comp (C) 1^{st} (z)) 1^{st} (f)$
111	92 96 110	3eqtr4d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}) \land z \in ({Base}_{C} \times {Base}_{D})) \land (f \in (x Hom (T) y) \land g \in (y Hom (T) z))) \to (x 2^{nd} (P) z) (g (⟨x, y⟩ comp (T) z) f) = (y 2^{nd} (P) z) (g) (⟨({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (x), ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (y)⟩ comp (C) ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (z)) (x 2^{nd} (P) y) (f)$
112	7 5 8 23 24 25 26 27 28 2 30 37 56 82 111	isfuncd	$⊢ φ \to ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (T Func C) 2^{nd} (P)$
113		df-br	$⊢ ({1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}) (T Func C) 2^{nd} (P) \leftrightarrow ⟨{1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}, 2^{nd} (P)⟩ \in (T Func C)$
114	112 113	sylib	$⊢ φ \to ⟨{1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}, 2^{nd} (P)⟩ \in (T Func C)$
115	22 114	eqeltrd	$⊢ φ \to P \in (T Func C)$

Metamath Proof Explorer

Theorem 1stfcl

Proof