prf1st

Description: Cancellation of pairing with first projection. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	prf1st.p	$⊢ P = F {⟨,⟩}_{F} G$
	prf1st.c	$⊢ φ \to F \in (C Func D)$
	prf1st.d	$⊢ φ \to G \in (C Func E)$
Assertion	prf1st	$⊢ φ \to (D {1^{st}}_{F} E) \circ_{func} P = F$

Proof

Step	Hyp	Ref	Expression
1		prf1st.p	$⊢ P = F {⟨,⟩}_{F} G$
2		prf1st.c	$⊢ φ \to F \in (C Func D)$
3		prf1st.d	$⊢ φ \to G \in (C Func E)$
4		eqid	$⊢ D \times_{c} E = D \times_{c} E$
5		eqid	$⊢ {Base}_{D} = {Base}_{D}$
6		eqid	$⊢ {Base}_{E} = {Base}_{E}$
7	4 5 6	xpcbas	$⊢ {Base}_{D} \times {Base}_{E} = {Base}_{(D \times_{c} E)}$
8		eqid	$⊢ Hom (D \times_{c} E) = Hom (D \times_{c} E)$
9		funcrcl	$⊢ F \in (C Func D) \to (C \in Cat \land D \in Cat)$
10	2 9	syl	$⊢ φ \to (C \in Cat \land D \in Cat)$
11	10	simprd	$⊢ φ \to D \in Cat$
12	11	adantr	$⊢ (φ \land x \in {Base}_{C}) \to D \in Cat$
13		funcrcl	$⊢ G \in (C Func E) \to (C \in Cat \land E \in Cat)$
14	3 13	syl	$⊢ φ \to (C \in Cat \land E \in Cat)$
15	14	simprd	$⊢ φ \to E \in Cat$
16	15	adantr	$⊢ (φ \land x \in {Base}_{C}) \to E \in Cat$
17		eqid	$⊢ D {1^{st}}_{F} E = D {1^{st}}_{F} E$
18		eqid	$⊢ {Base}_{C} = {Base}_{C}$
19		relfunc	$⊢ Rel (C Func D)$
20		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
21	19 2 20	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
22	18 5 21	funcf1	$⊢ φ \to 1^{st} (F) : {Base}_{C} ⟶ {Base}_{D}$
23	22	ffvelrnda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (F) (x) \in {Base}_{D}$
24		relfunc	$⊢ Rel (C Func E)$
25		1st2ndbr	$⊢ (Rel (C Func E) \land G \in (C Func E)) \to 1^{st} (G) (C Func E) 2^{nd} (G)$
26	24 3 25	sylancr	$⊢ φ \to 1^{st} (G) (C Func E) 2^{nd} (G)$
27	18 6 26	funcf1	$⊢ φ \to 1^{st} (G) : {Base}_{C} ⟶ {Base}_{E}$
28	27	ffvelrnda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (G) (x) \in {Base}_{E}$
29	23 28	opelxpd	$⊢ (φ \land x \in {Base}_{C}) \to ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \in ({Base}_{D} \times {Base}_{E})$
30	4 7 8 12 16 17 29	1stf1	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (D {1^{st}}_{F} E) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩) = 1^{st} (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩)$
31		fvex	$⊢ 1^{st} (F) (x) \in V$
32		fvex	$⊢ 1^{st} (G) (x) \in V$
33	31 32	op1st	$⊢ 1^{st} (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩) = 1^{st} (F) (x)$
34	30 33	eqtrdi	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (D {1^{st}}_{F} E) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩) = 1^{st} (F) (x)$
35	34	mpteq2dva	$⊢ φ \to (x \in {Base}_{C} ⟼ 1^{st} (D {1^{st}}_{F} E) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩)) = (x \in {Base}_{C} ⟼ 1^{st} (F) (x))$
36		eqid	$⊢ Hom (C) = Hom (C)$
37	1 18 36 2 3	prfval	$⊢ φ \to P = ⟨(x \in {Base}_{C} ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (h \in (x Hom (C) y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))⟩$
38		fvex	$⊢ {Base}_{C} \in V$
39	38	mptex	$⊢ (x \in {Base}_{C} ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩) \in V$
40	38 38	mpoex	$⊢ (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (h \in (x Hom (C) y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩)) \in V$
41	39 40	op1std	$⊢ P = ⟨(x \in {Base}_{C} ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (h \in (x Hom (C) y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))⟩ \to 1^{st} (P) = (x \in {Base}_{C} ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩)$
42	37 41	syl	$⊢ φ \to 1^{st} (P) = (x \in {Base}_{C} ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩)$
43		relfunc	$⊢ Rel ((D \times_{c} E) Func D)$
44	4 11 15 17	1stfcl	$⊢ φ \to D {1^{st}}_{F} E \in ((D \times_{c} E) Func D)$
45		1st2ndbr	$⊢ (Rel ((D \times_{c} E) Func D) \land D {1^{st}}_{F} E \in ((D \times_{c} E) Func D)) \to 1^{st} (D {1^{st}}_{F} E) ((D \times_{c} E) Func D) 2^{nd} (D {1^{st}}_{F} E)$
46	43 44 45	sylancr	$⊢ φ \to 1^{st} (D {1^{st}}_{F} E) ((D \times_{c} E) Func D) 2^{nd} (D {1^{st}}_{F} E)$
47	7 5 46	funcf1	$⊢ φ \to 1^{st} (D {1^{st}}_{F} E) : {Base}_{D} \times {Base}_{E} ⟶ {Base}_{D}$
48	47	feqmptd	$⊢ φ \to 1^{st} (D {1^{st}}_{F} E) = (u \in ({Base}_{D} \times {Base}_{E}) ⟼ 1^{st} (D {1^{st}}_{F} E) (u))$
49		fveq2	$⊢ u = ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩ \to 1^{st} (D {1^{st}}_{F} E) (u) = 1^{st} (D {1^{st}}_{F} E) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩)$
50	29 42 48 49	fmptco	$⊢ φ \to 1^{st} (D {1^{st}}_{F} E) \circ 1^{st} (P) = (x \in {Base}_{C} ⟼ 1^{st} (D {1^{st}}_{F} E) (⟨1^{st} (F) (x), 1^{st} (G) (x)⟩))$
51	22	feqmptd	$⊢ φ \to 1^{st} (F) = (x \in {Base}_{C} ⟼ 1^{st} (F) (x))$
52	35 50 51	3eqtr4d	$⊢ φ \to 1^{st} (D {1^{st}}_{F} E) \circ 1^{st} (P) = 1^{st} (F)$
53	11	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to D \in Cat$
54	15	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to E \in Cat$
55		relfunc	$⊢ Rel (C Func (D \times_{c} E))$
56	1 4 2 3	prfcl	$⊢ φ \to P \in (C Func (D \times_{c} E))$
57		1st2ndbr	$⊢ (Rel (C Func (D \times_{c} E)) \land P \in (C Func (D \times_{c} E))) \to 1^{st} (P) (C Func (D \times_{c} E)) 2^{nd} (P)$
58	55 56 57	sylancr	$⊢ φ \to 1^{st} (P) (C Func (D \times_{c} E)) 2^{nd} (P)$
59	18 7 58	funcf1	$⊢ φ \to 1^{st} (P) : {Base}_{C} ⟶ {Base}_{D} \times {Base}_{E}$
60	59	ffvelrnda	$⊢ (φ \land x \in {Base}_{C}) \to 1^{st} (P) (x) \in ({Base}_{D} \times {Base}_{E})$
61	60	adantrr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (P) (x) \in ({Base}_{D} \times {Base}_{E})$
62	61	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to 1^{st} (P) (x) \in ({Base}_{D} \times {Base}_{E})$
63	59	ffvelrnda	$⊢ (φ \land y \in {Base}_{C}) \to 1^{st} (P) (y) \in ({Base}_{D} \times {Base}_{E})$
64	63	adantrl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (P) (y) \in ({Base}_{D} \times {Base}_{E})$
65	64	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to 1^{st} (P) (y) \in ({Base}_{D} \times {Base}_{E})$
66	4 7 8 53 54 17 62 65	1stf2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to 1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y) = {1^{st} ↾}_{(1^{st} (P) (x) Hom (D \times_{c} E) 1^{st} (P) (y))}$
67	66	fveq1d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) ((x 2^{nd} (P) y) (f)) = ({1^{st} ↾}_{(1^{st} (P) (x) Hom (D \times_{c} E) 1^{st} (P) (y))}) ((x 2^{nd} (P) y) (f))$
68	58	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (P) (C Func (D \times_{c} E)) 2^{nd} (P)$
69		simprl	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x \in {Base}_{C}$
70		simprr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to y \in {Base}_{C}$
71	18 36 8 68 69 70	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (P) y) : x Hom (C) y ⟶ 1^{st} (P) (x) Hom (D \times_{c} E) 1^{st} (P) (y)$
72	71	ffvelrnda	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (P) y) (f) \in (1^{st} (P) (x) Hom (D \times_{c} E) 1^{st} (P) (y))$
73	72	fvresd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to ({1^{st} ↾}_{(1^{st} (P) (x) Hom (D \times_{c} E) 1^{st} (P) (y))}) ((x 2^{nd} (P) y) (f)) = 1^{st} ((x 2^{nd} (P) y) (f))$
74	2	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to F \in (C Func D)$
75	3	ad2antrr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to G \in (C Func E)$
76	69	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to x \in {Base}_{C}$
77	70	adantr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to y \in {Base}_{C}$
78		simpr	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to f \in (x Hom (C) y)$
79	1 18 36 74 75 76 77 78	prf2	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (x 2^{nd} (P) y) (f) = ⟨(x 2^{nd} (F) y) (f), (x 2^{nd} (G) y) (f)⟩$
80	79	fveq2d	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to 1^{st} ((x 2^{nd} (P) y) (f)) = 1^{st} (⟨(x 2^{nd} (F) y) (f), (x 2^{nd} (G) y) (f)⟩)$
81		fvex	$⊢ (x 2^{nd} (F) y) (f) \in V$
82		fvex	$⊢ (x 2^{nd} (G) y) (f) \in V$
83	81 82	op1st	$⊢ 1^{st} (⟨(x 2^{nd} (F) y) (f), (x 2^{nd} (G) y) (f)⟩) = (x 2^{nd} (F) y) (f)$
84	80 83	eqtrdi	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to 1^{st} ((x 2^{nd} (P) y) (f)) = (x 2^{nd} (F) y) (f)$
85	67 73 84	3eqtrd	$⊢ ((φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \land f \in (x Hom (C) y)) \to (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) ((x 2^{nd} (P) y) (f)) = (x 2^{nd} (F) y) (f)$
86	85	mpteq2dva	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (f \in (x Hom (C) y) ⟼ (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) ((x 2^{nd} (P) y) (f))) = (f \in (x Hom (C) y) ⟼ (x 2^{nd} (F) y) (f))$
87		eqid	$⊢ Hom (D) = Hom (D)$
88	46	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (D {1^{st}}_{F} E) ((D \times_{c} E) Func D) 2^{nd} (D {1^{st}}_{F} E)$
89	7 8 87 88 61 64	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) : 1^{st} (P) (x) Hom (D \times_{c} E) 1^{st} (P) (y) ⟶ 1^{st} (D {1^{st}}_{F} E) (1^{st} (P) (x)) Hom (D) 1^{st} (D {1^{st}}_{F} E) (1^{st} (P) (y))$
90		fcompt	$⊢ ((1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) : 1^{st} (P) (x) Hom (D \times_{c} E) 1^{st} (P) (y) ⟶ 1^{st} (D {1^{st}}_{F} E) (1^{st} (P) (x)) Hom (D) 1^{st} (D {1^{st}}_{F} E) (1^{st} (P) (y)) \land (x 2^{nd} (P) y) : x Hom (C) y ⟶ 1^{st} (P) (x) Hom (D \times_{c} E) 1^{st} (P) (y)) \to (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) \circ (x 2^{nd} (P) y) = (f \in (x Hom (C) y) ⟼ (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) ((x 2^{nd} (P) y) (f)))$
91	89 71 90	syl2anc	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) \circ (x 2^{nd} (P) y) = (f \in (x Hom (C) y) ⟼ (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) ((x 2^{nd} (P) y) (f)))$
92	21	adantr	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
93	18 36 87 92 69 70	funcf2	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (x 2^{nd} (F) y) : x Hom (C) y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
94	93	feqmptd	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to x 2^{nd} (F) y = (f \in (x Hom (C) y) ⟼ (x 2^{nd} (F) y) (f))$
95	86 91 94	3eqtr4d	$⊢ (φ \land (x \in {Base}_{C} \land y \in {Base}_{C})) \to (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) \circ (x 2^{nd} (P) y) = x 2^{nd} (F) y$
96	95	3impb	$⊢ (φ \land x \in {Base}_{C} \land y \in {Base}_{C}) \to (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) \circ (x 2^{nd} (P) y) = x 2^{nd} (F) y$
97	96	mpoeq3dva	$⊢ φ \to (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) \circ (x 2^{nd} (P) y)) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (F) y)$
98	18 21	funcfn2	$⊢ φ \to 2^{nd} (F) Fn ({Base}_{C} \times {Base}_{C})$
99		fnov	$⊢ 2^{nd} (F) Fn ({Base}_{C} \times {Base}_{C}) \leftrightarrow 2^{nd} (F) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (F) y)$
100	98 99	sylib	$⊢ φ \to 2^{nd} (F) = (x \in {Base}_{C}, y \in {Base}_{C} ⟼ x 2^{nd} (F) y)$
101	97 100	eqtr4d	$⊢ φ \to (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) \circ (x 2^{nd} (P) y)) = 2^{nd} (F)$
102	52 101	opeq12d	$⊢ φ \to ⟨1^{st} (D {1^{st}}_{F} E) \circ 1^{st} (P), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) \circ (x 2^{nd} (P) y))⟩ = ⟨1^{st} (F), 2^{nd} (F)⟩$
103	18 56 44	cofuval	$⊢ φ \to (D {1^{st}}_{F} E) \circ_{func} P = ⟨1^{st} (D {1^{st}}_{F} E) \circ 1^{st} (P), (x \in {Base}_{C}, y \in {Base}_{C} ⟼ (1^{st} (P) (x) 2^{nd} (D {1^{st}}_{F} E) 1^{st} (P) (y)) \circ (x 2^{nd} (P) y))⟩$
104		1st2nd	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
105	19 2 104	sylancr	$⊢ φ \to F = ⟨1^{st} (F), 2^{nd} (F)⟩$
106	102 103 105	3eqtr4d	$⊢ φ \to (D {1^{st}}_{F} E) \circ_{func} P = F$

Metamath Proof Explorer

Theorem prf1st

Proof