prf1st

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

	Ref	Expression
Hypotheses	prf1st.p	⊢ 𝑃 = ( 𝐹 ⟨,⟩_F 𝐺 )
	prf1st.c	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	prf1st.d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
Assertion	prf1st	⊢ ( 𝜑 → ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝑃 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		prf1st.p	⊢ 𝑃 = ( 𝐹 ⟨,⟩_F 𝐺 )
2		prf1st.c	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
3		prf1st.d	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
4		eqid	⊢ ( 𝐷 ×_c 𝐸 ) = ( 𝐷 ×_c 𝐸 )
5		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
6		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
7	4 5 6	xpcbas	⊢ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) = ( Base ‘ ( 𝐷 ×_c 𝐸 ) )
8		eqid	⊢ ( Hom ‘ ( 𝐷 ×_c 𝐸 ) ) = ( Hom ‘ ( 𝐷 ×_c 𝐸 ) )
9		funcrcl	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
10	2 9	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
11	10	simprd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐷 ∈ Cat )
13		funcrcl	⊢ ( 𝐺 ∈ ( 𝐶 Func 𝐸 ) → ( 𝐶 ∈ Cat ∧ 𝐸 ∈ Cat ) )
14	3 13	syl	⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐸 ∈ Cat ) )
15	14	simprd	⊢ ( 𝜑 → 𝐸 ∈ Cat )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐸 ∈ Cat )
17		eqid	⊢ ( 𝐷 1^st_F 𝐸 ) = ( 𝐷 1^st_F 𝐸 )
18		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
19		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
20		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
21	19 2 20	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
22	18 5 21	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
23	22	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
24		relfunc	⊢ Rel ( 𝐶 Func 𝐸 )
25		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
26	24 3 25	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) ( 𝐶 Func 𝐸 ) ( 2^nd ‘ 𝐺 ) )
27	18 6 26	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝐺 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐸 ) )
28	27	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐸 ) )
29	23 28	opelxpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
30	4 7 8 12 16 17 29	1stf1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) = ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
31		fvex	⊢ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ V
32		fvex	⊢ ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ∈ V
33	31 32	op1st	⊢ ( 1^st ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 )
34	30 33	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) = ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) )
35	34	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
36		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
37	1 18 36 2 3	prfval	⊢ ( 𝜑 → 𝑃 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ )
38		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
39	38	mptex	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) ∈ V
40	38 38	mpoex	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ∈ V
41	39 40	op1std	⊢ ( 𝑃 = ⟨ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ℎ ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ ℎ ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ ℎ ) ⟩ ) ) ⟩ → ( 1^st ‘ 𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
42	37 41	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
43		relfunc	⊢ Rel ( ( 𝐷 ×_c 𝐸 ) Func 𝐷 )
44	4 11 15 17	1stfcl	⊢ ( 𝜑 → ( 𝐷 1^st_F 𝐸 ) ∈ ( ( 𝐷 ×_c 𝐸 ) Func 𝐷 ) )
45		1st2ndbr	⊢ ( ( Rel ( ( 𝐷 ×_c 𝐸 ) Func 𝐷 ) ∧ ( 𝐷 1^st_F 𝐸 ) ∈ ( ( 𝐷 ×_c 𝐸 ) Func 𝐷 ) ) → ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 𝐷 ×_c 𝐸 ) Func 𝐷 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) )
46	43 44 45	sylancr	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 𝐷 ×_c 𝐸 ) Func 𝐷 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) )
47	7 5 46	funcf1	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) : ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) ⟶ ( Base ‘ 𝐷 ) )
48	47	feqmptd	⊢ ( 𝜑 → ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) ↦ ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ 𝑢 ) ) )
49		fveq2	⊢ ( 𝑢 = ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ → ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ 𝑢 ) = ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) )
50	29 42 48 49	fmptco	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ∘ ( 1^st ‘ 𝑃 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ ⟨ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) , ( ( 1^st ‘ 𝐺 ) ‘ 𝑥 ) ⟩ ) ) )
51	22	feqmptd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
52	35 50 51	3eqtr4d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ∘ ( 1^st ‘ 𝑃 ) ) = ( 1^st ‘ 𝐹 ) )
53	11	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐷 ∈ Cat )
54	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐸 ∈ Cat )
55		relfunc	⊢ Rel ( 𝐶 Func ( 𝐷 ×_c 𝐸 ) )
56	1 4 2 3	prfcl	⊢ ( 𝜑 → 𝑃 ∈ ( 𝐶 Func ( 𝐷 ×_c 𝐸 ) ) )
57		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func ( 𝐷 ×_c 𝐸 ) ) ∧ 𝑃 ∈ ( 𝐶 Func ( 𝐷 ×_c 𝐸 ) ) ) → ( 1^st ‘ 𝑃 ) ( 𝐶 Func ( 𝐷 ×_c 𝐸 ) ) ( 2^nd ‘ 𝑃 ) )
58	55 56 57	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) ( 𝐶 Func ( 𝐷 ×_c 𝐸 ) ) ( 2^nd ‘ 𝑃 ) )
59	18 7 58	funcf1	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) : ( Base ‘ 𝐶 ) ⟶ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
60	59	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
61	60	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
62	61	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
63	59	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
64	63	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
65	64	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ∈ ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐸 ) ) )
66	4 7 8 53 54 17 62 65	1stf2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) = ( 1^st ↾ ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×_c 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ) )
67	66	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 1^st ↾ ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×_c 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) )
68	58	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑃 ) ( 𝐶 Func ( 𝐷 ×_c 𝐸 ) ) ( 2^nd ‘ 𝑃 ) )
69		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
70		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
71	18 36 8 68 69 70	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×_c 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) )
72	71	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ∈ ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×_c 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) )
73	72	fvresd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 1^st ↾ ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×_c 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( 1^st ‘ ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) )
74	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
75	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
76	69	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
77	70	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
78		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) )
79	1 18 36 74 75 76 77 78	prf2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) = ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ )
80	79	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1^st ‘ ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( 1^st ‘ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ ) )
81		fvex	⊢ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ∈ V
82		fvex	⊢ ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ∈ V
83	81 82	op1st	⊢ ( 1^st ‘ ⟨ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) , ( ( 𝑥 ( 2^nd ‘ 𝐺 ) 𝑦 ) ‘ 𝑓 ) ⟩ ) = ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 )
84	80 83	eqtrdi	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( 1^st ‘ ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) )
85	67 73 84	3eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ) → ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) = ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) )
86	85	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
87		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
88	46	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 𝐷 ×_c 𝐸 ) Func 𝐷 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) )
89	7 8 87 88 61 64	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) : ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×_c 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ⟶ ( ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ) )
90		fcompt	⊢ ( ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) : ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×_c 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ⟶ ( ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ‘ ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ) ∧ ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( Hom ‘ ( 𝐷 ×_c 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ) → ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) ) )
91	89 71 90	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ‘ ( ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ‘ 𝑓 ) ) ) )
92	21	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
93	18 36 87 92 69 70	funcf2	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑦 ) ) )
94	93	feqmptd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) = ( 𝑓 ∈ ( 𝑥 ( Hom ‘ 𝐶 ) 𝑦 ) ↦ ( ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ‘ 𝑓 ) ) )
95	86 91 94	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ) = ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
96	95	3impb	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ) = ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) )
97	96	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
98	18 21	funcfn2	⊢ ( 𝜑 → ( 2^nd ‘ 𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) )
99		fnov	⊢ ( ( 2^nd ‘ 𝐹 ) Fn ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐶 ) ) ↔ ( 2^nd ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
100	98 99	sylib	⊢ ( 𝜑 → ( 2^nd ‘ 𝐹 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑥 ( 2^nd ‘ 𝐹 ) 𝑦 ) ) )
101	97 100	eqtr4d	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ) ) = ( 2^nd ‘ 𝐹 ) )
102	52 101	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ∘ ( 1^st ‘ 𝑃 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ) ) ⟩ = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
103	18 56 44	cofuval	⊢ ( 𝜑 → ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝑃 ) = ⟨ ( ( 1^st ‘ ( 𝐷 1^st_F 𝐸 ) ) ∘ ( 1^st ‘ 𝑃 ) ) , ( 𝑥 ∈ ( Base ‘ 𝐶 ) , 𝑦 ∈ ( Base ‘ 𝐶 ) ↦ ( ( ( ( 1^st ‘ 𝑃 ) ‘ 𝑥 ) ( 2^nd ‘ ( 𝐷 1^st_F 𝐸 ) ) ( ( 1^st ‘ 𝑃 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 2^nd ‘ 𝑃 ) 𝑦 ) ) ) ⟩ )
104		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
105	19 2 104	sylancr	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
106	102 103 105	3eqtr4d	⊢ ( 𝜑 → ( ( 𝐷 1^st_F 𝐸 ) ∘_func 𝑃 ) = 𝐹 )

Metamath Proof Explorer

Theorem prf1st

Proof