Theorem yonedalem1

Description: Lemma for yoneda . (Contributed by Mario Carneiro, 28-Jan-2017)

	Ref	Expression
Hypotheses	yoneda.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
	yoneda.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	yoneda.1	⊢ 1 = ( Id ‘ 𝐶 )
	yoneda.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	yoneda.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	yoneda.t	⊢ 𝑇 = ( SetCat ‘ 𝑉 )
	yoneda.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
	yoneda.h	⊢ 𝐻 = ( HomF ‘ 𝑄 )
	yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×c 𝑂 ) FuncCat 𝑇 )
	yoneda.e	⊢ 𝐸 = ( 𝑂 evalF 𝑆 )
	yoneda.z	⊢ 𝑍 = ( 𝐻 ∘func ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) )
	yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
	yoneda.u	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
	yoneda.v	⊢ ( 𝜑 → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
Assertion	yonedalem1	⊢ ( 𝜑 → ( 𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		yoneda.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
2		yoneda.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		yoneda.1	⊢ 1 = ( Id ‘ 𝐶 )
4		yoneda.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
5		yoneda.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
6		yoneda.t	⊢ 𝑇 = ( SetCat ‘ 𝑉 )
7		yoneda.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
8		yoneda.h	⊢ 𝐻 = ( HomF ‘ 𝑄 )
9		yoneda.r	⊢ 𝑅 = ( ( 𝑄 ×c 𝑂 ) FuncCat 𝑇 )
10		yoneda.e	⊢ 𝐸 = ( 𝑂 evalF 𝑆 )
11		yoneda.z	⊢ 𝑍 = ( 𝐻 ∘func ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) )
12		yoneda.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13		yoneda.w	⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
14		yoneda.u	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
15		yoneda.v	⊢ ( 𝜑 → ( ran ( Homf ‘ 𝑄 ) ∪ 𝑈 ) ⊆ 𝑉 )
16		eqid	⊢ ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) = ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) )
17		eqid	⊢ ( ( oppCat ‘ 𝑄 ) ×c 𝑄 ) = ( ( oppCat ‘ 𝑄 ) ×c 𝑄 )
18		eqid	⊢ ( 𝑄 ×c 𝑂 ) = ( 𝑄 ×c 𝑂 )
19	4	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
20	12 19	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
21	15	unssbd	⊢ ( 𝜑 → 𝑈 ⊆ 𝑉 )
22	13 21	ssexd	⊢ ( 𝜑 → 𝑈 ∈ V )
23	5	setccat	⊢ ( 𝑈 ∈ V → 𝑆 ∈ Cat )
24	22 23	syl	⊢ ( 𝜑 → 𝑆 ∈ Cat )
25	7 20 24	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
26		eqid	⊢ ( 𝑄 2ndF 𝑂 ) = ( 𝑄 2ndF 𝑂 )
27	18 25 20 26	2ndfcl	⊢ ( 𝜑 → ( 𝑄 2ndF 𝑂 ) ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑂 ) )
28		eqid	⊢ ( oppCat ‘ 𝑄 ) = ( oppCat ‘ 𝑄 )
29		relfunc	⊢ Rel ( 𝐶 Func 𝑄 )
30	1 12 4 5 7 22 14	yoncl	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝑄 ) )
31		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝑄 ) ∧ 𝑌 ∈ ( 𝐶 Func 𝑄 ) ) → ( 1st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ 𝑌 ) )
32	29 30 31	sylancr	⊢ ( 𝜑 → ( 1st ‘ 𝑌 ) ( 𝐶 Func 𝑄 ) ( 2nd ‘ 𝑌 ) )
33	4 28 32	funcoppc	⊢ ( 𝜑 → ( 1st ‘ 𝑌 ) ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) tpos ( 2nd ‘ 𝑌 ) )
34		df-br	⊢ ( ( 1st ‘ 𝑌 ) ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) tpos ( 2nd ‘ 𝑌 ) ↔ ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∈ ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) )
35	33 34	sylib	⊢ ( 𝜑 → ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∈ ( 𝑂 Func ( oppCat ‘ 𝑄 ) ) )
36	27 35	cofucl	⊢ ( 𝜑 → ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ∈ ( ( 𝑄 ×c 𝑂 ) Func ( oppCat ‘ 𝑄 ) ) )
37		eqid	⊢ ( 𝑄 1stF 𝑂 ) = ( 𝑄 1stF 𝑂 )
38	18 25 20 37	1stfcl	⊢ ( 𝜑 → ( 𝑄 1stF 𝑂 ) ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑄 ) )
39	16 17 36 38	prfcl	⊢ ( 𝜑 → ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) ∈ ( ( 𝑄 ×c 𝑂 ) Func ( ( oppCat ‘ 𝑄 ) ×c 𝑄 ) ) )
40	15	unssad	⊢ ( 𝜑 → ran ( Homf ‘ 𝑄 ) ⊆ 𝑉 )
41	8 28 6 25 13 40	hofcl	⊢ ( 𝜑 → 𝐻 ∈ ( ( ( oppCat ‘ 𝑄 ) ×c 𝑄 ) Func 𝑇 ) )
42	39 41	cofucl	⊢ ( 𝜑 → ( 𝐻 ∘func ( ( ⟨ ( 1st ‘ 𝑌 ) , tpos ( 2nd ‘ 𝑌 ) ⟩ ∘func ( 𝑄 2ndF 𝑂 ) ) ⟨,⟩F ( 𝑄 1stF 𝑂 ) ) ) ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) )
43	11 42	eqeltrid	⊢ ( 𝜑 → 𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) )
44	6 5 13 21	funcsetcres2	⊢ ( 𝜑 → ( ( 𝑄 ×c 𝑂 ) Func 𝑆 ) ⊆ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) )
45	10 7 20 24	evlfcl	⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑆 ) )
46	44 45	sseldd	⊢ ( 𝜑 → 𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) )
47	43 46	jca	⊢ ( 𝜑 → ( 𝑍 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ∧ 𝐸 ∈ ( ( 𝑄 ×c 𝑂 ) Func 𝑇 ) ) )