Theorem 2ndfval

Description: Value of the first projection functor. (Contributed by Mario Carneiro, 11-Jan-2017)

	Ref	Expression
Hypotheses	1stfval.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
	1stfval.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
	1stfval.h	⊢ 𝐻 = ( Hom ‘ 𝑇 )
	1stfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	1stfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
	2ndfval.p	⊢ 𝑄 = ( 𝐶 2ndF 𝐷 )
Assertion	2ndfval	⊢ ( 𝜑 → 𝑄 = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		1stfval.t	⊢ 𝑇 = ( 𝐶 ×c 𝐷 )
2		1stfval.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
3		1stfval.h	⊢ 𝐻 = ( Hom ‘ 𝑇 )
4		1stfval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		1stfval.d	⊢ ( 𝜑 → 𝐷 ∈ Cat )
6		2ndfval.p	⊢ 𝑄 = ( 𝐶 2ndF 𝐷 )
7		fvex	⊢ ( Base ‘ 𝑐 ) ∈ V
8		fvex	⊢ ( Base ‘ 𝑑 ) ∈ V
9	7 8	xpex	⊢ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ∈ V
10	9	a1i	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) ∈ V )
11		simpl	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → 𝑐 = 𝐶 )
12	11	fveq2d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
13		simpr	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
14	13	fveq2d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( Base ‘ 𝑑 ) = ( Base ‘ 𝐷 ) )
15	12 14	xpeq12d	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
16		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
17		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
18	1 16 17	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝑇 )
19	18 2	eqtr4i	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = 𝐵
20	15 19	eqtrdi	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) = 𝐵 )
21		simpr	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑏 = 𝐵 )
22	21	reseq2d	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 2nd ↾ 𝑏 ) = ( 2nd ↾ 𝐵 ) )
23		simpll	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑐 = 𝐶 )
24		simplr	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → 𝑑 = 𝐷 )
25	23 24	oveq12d	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑐 ×c 𝑑 ) = ( 𝐶 ×c 𝐷 ) )
26	25 1	eqtr4di	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑐 ×c 𝑑 ) = 𝑇 )
27	26	fveq2d	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) = ( Hom ‘ 𝑇 ) )
28	27 3	eqtr4di	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) = 𝐻 )
29	28	oveqd	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) = ( 𝑥 𝐻 𝑦 ) )
30	29	reseq2d	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) ) = ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) )
31	21 21 30	mpoeq123dv	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) )
32	22 31	opeq12d	⊢ ( ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) ∧ 𝑏 = 𝐵 ) → ⟨ ( 2nd ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) ) ) ⟩ = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
33	10 20 32	csbied2	⊢ ( ( 𝑐 = 𝐶 ∧ 𝑑 = 𝐷 ) → ⦋ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) / 𝑏 ⦌ ⟨ ( 2nd ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) ) ) ⟩ = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
34		df-2ndf	⊢ 2ndF = ( 𝑐 ∈ Cat , 𝑑 ∈ Cat ↦ ⦋ ( ( Base ‘ 𝑐 ) × ( Base ‘ 𝑑 ) ) / 𝑏 ⦌ ⟨ ( 2nd ↾ 𝑏 ) , ( 𝑥 ∈ 𝑏 , 𝑦 ∈ 𝑏 ↦ ( 2nd ↾ ( 𝑥 ( Hom ‘ ( 𝑐 ×c 𝑑 ) ) 𝑦 ) ) ) ⟩ )
35		opex	⊢ ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ ∈ V
36	33 34 35	ovmpoa	⊢ ( ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) → ( 𝐶 2ndF 𝐷 ) = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
37	4 5 36	syl2anc	⊢ ( 𝜑 → ( 𝐶 2ndF 𝐷 ) = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )
38	6 37	syl5eq	⊢ ( 𝜑 → 𝑄 = ⟨ ( 2nd ↾ 𝐵 ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 2nd ↾ ( 𝑥 𝐻 𝑦 ) ) ) ⟩ )