prfval

Description: Value of the pairing functor. (Contributed by Mario Carneiro, 12-Jan-2017)

	Ref	Expression
Hypotheses	prfval.k	$⊢ P = F {⟨,⟩}_{F} G$
	prfval.b	$⊢ B = {Base}_{C}$
	prfval.h	$⊢ H = Hom (C)$
	prfval.c	$⊢ φ \to F \in (C Func D)$
	prfval.d	$⊢ φ \to G \in (C Func E)$
Assertion	prfval	$⊢ φ \to P = ⟨(x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩), (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))⟩$

Proof

Step	Hyp	Ref	Expression
1		prfval.k	$⊢ P = F {⟨,⟩}_{F} G$
2		prfval.b	$⊢ B = {Base}_{C}$
3		prfval.h	$⊢ H = Hom (C)$
4		prfval.c	$⊢ φ \to F \in (C Func D)$
5		prfval.d	$⊢ φ \to G \in (C Func E)$
6		df-prf	$⊢ {⟨,⟩}_{F} = (f \in V, g \in V ⟼ ⦋ dom 1^{st} (f) / b ⦌ ⟨(x \in b ⟼ ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩), (x \in b, y \in b ⟼ (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩))⟩)$
7	6	a1i	$⊢ φ \to {⟨,⟩}_{F} = (f \in V, g \in V ⟼ ⦋ dom 1^{st} (f) / b ⦌ ⟨(x \in b ⟼ ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩), (x \in b, y \in b ⟼ (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩))⟩)$
8		fvex	$⊢ 1^{st} (f) \in V$
9	8	dmex	$⊢ dom 1^{st} (f) \in V$
10	9	a1i	$⊢ (φ \land (f = F \land g = G)) \to dom 1^{st} (f) \in V$
11		simprl	$⊢ (φ \land (f = F \land g = G)) \to f = F$
12	11	fveq2d	$⊢ (φ \land (f = F \land g = G)) \to 1^{st} (f) = 1^{st} (F)$
13	12	dmeqd	$⊢ (φ \land (f = F \land g = G)) \to dom 1^{st} (f) = dom 1^{st} (F)$
14		eqid	$⊢ {Base}_{D} = {Base}_{D}$
15		relfunc	$⊢ Rel (C Func D)$
16		1st2ndbr	$⊢ (Rel (C Func D) \land F \in (C Func D)) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
17	15 4 16	sylancr	$⊢ φ \to 1^{st} (F) (C Func D) 2^{nd} (F)$
18	2 14 17	funcf1	$⊢ φ \to 1^{st} (F) : B ⟶ {Base}_{D}$
19	18	fdmd	$⊢ φ \to dom 1^{st} (F) = B$
20	19	adantr	$⊢ (φ \land (f = F \land g = G)) \to dom 1^{st} (F) = B$
21	13 20	eqtrd	$⊢ (φ \land (f = F \land g = G)) \to dom 1^{st} (f) = B$
22		simpr	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to b = B$
23		simplrl	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to f = F$
24	23	fveq2d	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to 1^{st} (f) = 1^{st} (F)$
25	24	fveq1d	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to 1^{st} (f) (x) = 1^{st} (F) (x)$
26		simplrr	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to g = G$
27	26	fveq2d	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to 1^{st} (g) = 1^{st} (G)$
28	27	fveq1d	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to 1^{st} (g) (x) = 1^{st} (G) (x)$
29	25 28	opeq12d	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩ = ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩$
30	22 29	mpteq12dv	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to (x \in b ⟼ ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩) = (x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩)$
31		eqidd	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩) = (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩)$
32	22 22 31	mpoeq123dv	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to (x \in b, y \in b ⟼ (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩)) = (x \in B, y \in B ⟼ (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩))$
33	23	ad2antrr	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to f = F$
34	33	fveq2d	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to 2^{nd} (f) = 2^{nd} (F)$
35	34	oveqd	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to x 2^{nd} (f) y = x 2^{nd} (F) y$
36	35	dmeqd	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to dom (x 2^{nd} (f) y) = dom (x 2^{nd} (F) y)$
37		eqid	$⊢ Hom (D) = Hom (D)$
38	17	ad4antr	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to 1^{st} (F) (C Func D) 2^{nd} (F)$
39		simplr	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to x \in B$
40		simpr	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to y \in B$
41	2 3 37 38 39 40	funcf2	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to (x 2^{nd} (F) y) : x H y ⟶ 1^{st} (F) (x) Hom (D) 1^{st} (F) (y)$
42	41	fdmd	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to dom (x 2^{nd} (F) y) = x H y$
43	36 42	eqtrd	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to dom (x 2^{nd} (f) y) = x H y$
44	35	fveq1d	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to (x 2^{nd} (f) y) (h) = (x 2^{nd} (F) y) (h)$
45	26	ad2antrr	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to g = G$
46	45	fveq2d	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to 2^{nd} (g) = 2^{nd} (G)$
47	46	oveqd	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to x 2^{nd} (g) y = x 2^{nd} (G) y$
48	47	fveq1d	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to (x 2^{nd} (g) y) (h) = (x 2^{nd} (G) y) (h)$
49	44 48	opeq12d	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩ = ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩$
50	43 49	mpteq12dv	$⊢ ((((φ \land (f = F \land g = G)) \land b = B) \land x \in B) \land y \in B) \to (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩) = (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩)$
51	50	3impa	$⊢ (((φ \land (f = F \land g = G)) \land b = B) \land x \in B \land y \in B) \to (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩) = (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩)$
52	51	mpoeq3dva	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to (x \in B, y \in B ⟼ (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩)) = (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))$
53	32 52	eqtrd	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to (x \in b, y \in b ⟼ (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩)) = (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))$
54	30 53	opeq12d	$⊢ ((φ \land (f = F \land g = G)) \land b = B) \to ⟨(x \in b ⟼ ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩), (x \in b, y \in b ⟼ (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩))⟩ = ⟨(x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩), (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))⟩$
55	10 21 54	csbied2	$⊢ (φ \land (f = F \land g = G)) \to ⦋ dom 1^{st} (f) / b ⦌ ⟨(x \in b ⟼ ⟨1^{st} (f) (x), 1^{st} (g) (x)⟩), (x \in b, y \in b ⟼ (h \in dom (x 2^{nd} (f) y) ⟼ ⟨(x 2^{nd} (f) y) (h), (x 2^{nd} (g) y) (h)⟩))⟩ = ⟨(x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩), (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))⟩$
56	4	elexd	$⊢ φ \to F \in V$
57	5	elexd	$⊢ φ \to G \in V$
58		opex	$⊢ ⟨(x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩), (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))⟩ \in V$
59	58	a1i	$⊢ φ \to ⟨(x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩), (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))⟩ \in V$
60	7 55 56 57 59	ovmpod	$⊢ φ \to F {⟨,⟩}_{F} G = ⟨(x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩), (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))⟩$
61	1 60	syl5eq	$⊢ φ \to P = ⟨(x \in B ⟼ ⟨1^{st} (F) (x), 1^{st} (G) (x)⟩), (x \in B, y \in B ⟼ (h \in (x H y) ⟼ ⟨(x 2^{nd} (F) y) (h), (x 2^{nd} (G) y) (h)⟩))⟩$

Metamath Proof Explorer

Theorem prfval

Proof