2ndfcl

Description: The second projection functor is a functor onto the right 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$
	2ndfcl.p	$⊢ Q = C {2^{nd}}_{F} D$
Assertion	2ndfcl	$⊢ φ \to Q \in (T Func D)$

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		2ndfcl.p	$⊢ Q = C {2^{nd}}_{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	2ndfval	$⊢ φ \to Q = ⟨{2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}, (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {2^{nd} ↾}_{(x Hom (T) y)})⟩$
10		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
11		fofun	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to Fun 2^{nd}$
12	10 11	ax-mp	$⊢ Fun 2^{nd}$
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 2^{nd} \land {Base}_{C} \times {Base}_{D} \in V) \to {2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})} \in V$
17	12 15 16	mp2an	$⊢ {2^{nd} ↾}_{({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}) ⟼ {2^{nd} ↾}_{(x Hom (T) y)}) \in V$
19	17 18	op2ndd	$⊢ Q = ⟨{2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}, (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {2^{nd} ↾}_{(x Hom (T) y)})⟩ \to 2^{nd} (Q) = (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {2^{nd} ↾}_{(x Hom (T) y)})$
20	9 19	syl	$⊢ φ \to 2^{nd} (Q) = (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {2^{nd} ↾}_{(x Hom (T) y)})$
21	20	opeq2d	$⊢ φ \to ⟨{2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}, 2^{nd} (Q)⟩ = ⟨{2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}, (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {2^{nd} ↾}_{(x Hom (T) y)})⟩$
22	9 21	eqtr4d	$⊢ φ \to Q = ⟨{2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}, 2^{nd} (Q)⟩$
23		eqid	$⊢ Hom (D) = Hom (D)$
24		eqid	$⊢ Id (T) = Id (T)$
25		eqid	$⊢ Id (D) = Id (D)$
26		eqid	$⊢ comp (T) = comp (T)$
27		eqid	$⊢ comp (D) = comp (D)$
28	1 2 3	xpccat	$⊢ φ \to T \in Cat$
29		f2ndres	$⊢ ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) : {Base}_{C} \times {Base}_{D} ⟶ {Base}_{D}$
30	29	a1i	$⊢ φ \to ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) : {Base}_{C} \times {Base}_{D} ⟶ {Base}_{D}$
31		eqid	$⊢ (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {2^{nd} ↾}_{(x Hom (T) y)}) = (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {2^{nd} ↾}_{(x Hom (T) y)})$
32		ovex	$⊢ x Hom (T) y \in V$
33		resfunexg	$⊢ (Fun 2^{nd} \land x Hom (T) y \in V) \to {2^{nd} ↾}_{(x Hom (T) y)} \in V$
34	12 32 33	mp2an	$⊢ {2^{nd} ↾}_{(x Hom (T) y)} \in V$
35	31 34	fnmpoi	$⊢ (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {2^{nd} ↾}_{(x Hom (T) y)}) Fn (({Base}_{C} \times {Base}_{D}) \times ({Base}_{C} \times {Base}_{D}))$
36	20	fneq1d	$⊢ φ \to (2^{nd} (Q) 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}) ⟼ {2^{nd} ↾}_{(x Hom (T) y)}) Fn (({Base}_{C} \times {Base}_{D}) \times ({Base}_{C} \times {Base}_{D})))$
37	35 36	mpbiri	$⊢ φ \to 2^{nd} (Q) Fn (({Base}_{C} \times {Base}_{D}) \times ({Base}_{C} \times {Base}_{D}))$
38		f2ndres	$⊢ ({2^{nd} ↾}_{((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)) ⟶ 2^{nd} (x) Hom (D) 2^{nd} (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	2ndf2	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to x 2^{nd} (Q) y = {2^{nd} ↾}_{(x Hom (T) y)}$
44		eqid	$⊢ Hom (C) = Hom (C)$
45	1 7 44 23 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 {2^{nd} ↾}_{(x Hom (T) y)} = {2^{nd} ↾}_{((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} (Q) y = {2^{nd} ↾}_{((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} (Q) y) : (1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟶ 2^{nd} (x) Hom (D) 2^{nd} (y) \leftrightarrow ({2^{nd} ↾}_{((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)) ⟶ 2^{nd} (x) Hom (D) 2^{nd} (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} (Q) y) : (1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟶ 2^{nd} (x) Hom (D) 2^{nd} (y)$
50		fvres	$⊢ x \in ({Base}_{C} \times {Base}_{D}) \to ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) = 2^{nd} (x)$
51	50	ad2antrl	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) = 2^{nd} (x)$
52		fvres	$⊢ y \in ({Base}_{C} \times {Base}_{D}) \to ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (y) = 2^{nd} (y)$
53	52	ad2antll	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (y) = 2^{nd} (y)$
54	51 53	oveq12d	$⊢ (φ \land (x \in ({Base}_{C} \times {Base}_{D}) \land y \in ({Base}_{C} \times {Base}_{D}))) \to ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) Hom (D) ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (y) = 2^{nd} (x) Hom (D) 2^{nd} (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} (Q) y) : x Hom (T) y ⟶ ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) Hom (D) ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (y) \leftrightarrow (x 2^{nd} (Q) y) : (1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y)) ⟶ 2^{nd} (x) Hom (D) 2^{nd} (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} (Q) y) : x Hom (T) y ⟶ ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) Hom (D) ({2^{nd} ↾}_{({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 ({2^{nd} ↾}_{(x Hom (T) x)}) (Id (T) (x)) = 2^{nd} (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 (C) = Id (C)$
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 66 25 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	op2ndd	$⊢ Id (T) (x) = ⟨Id (C) (1^{st} (x)), Id (D) (2^{nd} (x))⟩ \to 2^{nd} (Id (T) (x)) = Id (D) (2^{nd} (x))$
76	72 75	syl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to 2^{nd} (Id (T) (x)) = Id (D) (2^{nd} (x))$
77	60 76	eqtrd	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to ({2^{nd} ↾}_{(x Hom (T) x)}) (Id (T) (x)) = Id (D) (2^{nd} (x))$
78	1 7 8 64 65 4 58 58	2ndf2	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to x 2^{nd} (Q) x = {2^{nd} ↾}_{(x Hom (T) x)}$
79	78	fveq1d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to (x 2^{nd} (Q) x) (Id (T) (x)) = ({2^{nd} ↾}_{(x Hom (T) x)}) (Id (T) (x))$
80	50	adantl	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) = 2^{nd} (x)$
81	80	fveq2d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to Id (D) (({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x)) = Id (D) (2^{nd} (x))$
82	77 79 81	3eqtr4d	$⊢ (φ \land x \in ({Base}_{C} \times {Base}_{D})) \to (x 2^{nd} (Q) x) (Id (T) (x)) = Id (D) (({2^{nd} ↾}_{({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 ({2^{nd} ↾}_{(x Hom (T) z)}) (g (⟨x, y⟩ comp (T) z) f) = 2^{nd} (g (⟨x, y⟩ comp (T) z) f)$
91	1 7 8 26 84 85 86 87 88 27	xpcco2nd	$⊢ (φ \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 2^{nd} (g (⟨x, y⟩ comp (T) z) f) = 2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (D) 2^{nd} (z)) 2^{nd} (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 ({2^{nd} ↾}_{(x Hom (T) z)}) (g (⟨x, y⟩ comp (T) z) f) = 2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (D) 2^{nd} (z)) 2^{nd} (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	2ndf2	$⊢ (φ \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} (Q) z = {2^{nd} ↾}_{(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} (Q) z) (g (⟨x, y⟩ comp (T) z) f) = ({2^{nd} ↾}_{(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 ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x) = 2^{nd} (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 ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (y) = 2^{nd} (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 ⟨({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x), ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (y)⟩ = ⟨2^{nd} (x), 2^{nd} (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 ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (z) = 2^{nd} (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 ⟨({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x), ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (y)⟩ comp (D) ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (z) = ⟨2^{nd} (x), 2^{nd} (y)⟩ comp (D) 2^{nd} (z)$
102	1 7 8 93 94 4 85 86	2ndf2	$⊢ (φ \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} (Q) z = {2^{nd} ↾}_{(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} (Q) z) (g) = ({2^{nd} ↾}_{(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 ({2^{nd} ↾}_{(y Hom (T) z)}) (g) = 2^{nd} (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} (Q) z) (g) = 2^{nd} (g)$
106	1 7 8 93 94 4 84 85	2ndf2	$⊢ (φ \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} (Q) y = {2^{nd} ↾}_{(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} (Q) y) (f) = ({2^{nd} ↾}_{(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 ({2^{nd} ↾}_{(x Hom (T) y)}) (f) = 2^{nd} (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} (Q) y) (f) = 2^{nd} (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} (Q) z) (g) (⟨({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x), ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (y)⟩ comp (D) ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (z)) (x 2^{nd} (Q) y) (f) = 2^{nd} (g) (⟨2^{nd} (x), 2^{nd} (y)⟩ comp (D) 2^{nd} (z)) 2^{nd} (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} (Q) z) (g (⟨x, y⟩ comp (T) z) f) = (y 2^{nd} (Q) z) (g) (⟨({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (x), ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (y)⟩ comp (D) ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (z)) (x 2^{nd} (Q) y) (f)$
112	7 6 8 23 24 25 26 27 28 3 30 37 56 82 111	isfuncd	$⊢ φ \to ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (T Func D) 2^{nd} (Q)$
113		df-br	$⊢ ({2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}) (T Func D) 2^{nd} (Q) \leftrightarrow ⟨{2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}, 2^{nd} (Q)⟩ \in (T Func D)$
114	112 113	sylib	$⊢ φ \to ⟨{2^{nd} ↾}_{({Base}_{C} \times {Base}_{D})}, 2^{nd} (Q)⟩ \in (T Func D)$
115	22 114	eqeltrd	$⊢ φ \to Q \in (T Func D)$

Metamath Proof Explorer

Theorem 2ndfcl

Proof