xpccofval

Description: Value of composition in the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017) (Proof shortened by AV, 2-Mar-2024)

	Ref	Expression
Hypotheses	xpccofval.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
	xpccofval.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
	xpccofval.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
	xpccofval.o1	⊢ · = ( comp ‘ 𝐶 )
	xpccofval.o2	⊢ ∙ = ( comp ‘ 𝐷 )
	xpccofval.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
Assertion	xpccofval	⊢ 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		xpccofval.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
2		xpccofval.b	⊢ 𝐵 = ( Base ‘ 𝑇 )
3		xpccofval.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
4		xpccofval.o1	⊢ · = ( comp ‘ 𝐶 )
5		xpccofval.o2	⊢ ∙ = ( comp ‘ 𝐷 )
6		xpccofval.o	⊢ 𝑂 = ( comp ‘ 𝑇 )
7		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
9		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
10		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
11		simpl	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝐶 ∈ V )
12		simpr	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝐷 ∈ V )
13	1 7 8	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝑇 )
14	2 13	eqtr4i	⊢ 𝐵 = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) )
15	14	a1i	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝐵 = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
16	1 2 9 10 3	xpchomfval	⊢ 𝐾 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) )
17	16	a1i	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝐾 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) )
18		eqidd	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) )
19	1 7 8 9 10 4 5 11 12 15 17 18	xpcval	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝑇 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ } )
20		catstr	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ } Struct ⟨ 1 , ; 1 5 ⟩
21		ccoid	⊢ comp = Slot ( comp ‘ ndx )
22		snsstp3	⊢ { ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ } ⊆ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( Hom ‘ ndx ) , 𝐾 ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ⟩ }
23	2	fvexi	⊢ 𝐵 ∈ V
24	23 23	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
25	24 23	mpoex	⊢ ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ∈ V
26	25	a1i	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) ∈ V )
27	19 20 21 22 26 6	strfv3	⊢ ( ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) )
28		fnxpc	⊢ ×_c Fn ( V × V )
29	28	fndmi	⊢ dom ×_c = ( V × V )
30	29	ndmov	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝐶 ×_c 𝐷 ) = ∅ )
31	1 30	syl5eq	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝑇 = ∅ )
32	31	fveq2d	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( comp ‘ 𝑇 ) = ( comp ‘ ∅ ) )
33	21	str0	⊢ ∅ = ( comp ‘ ∅ )
34	32 6 33	3eqtr4g	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝑂 = ∅ )
35	31	fveq2d	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( Base ‘ 𝑇 ) = ( Base ‘ ∅ ) )
36		base0	⊢ ∅ = ( Base ‘ ∅ )
37	35 2 36	3eqtr4g	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝐵 = ∅ )
38	37	olcd	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( ( 𝐵 × 𝐵 ) = ∅ ∨ 𝐵 = ∅ ) )
39		0mpo0	⊢ ( ( ( 𝐵 × 𝐵 ) = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) = ∅ )
40	38 39	syl	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) = ∅ )
41	34 40	eqtr4d	⊢ ( ¬ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) → 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) ) )
42	27 41	pm2.61i	⊢ 𝑂 = ( 𝑥 ∈ ( 𝐵 × 𝐵 ) , 𝑦 ∈ 𝐵 ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) 𝐾 𝑦 ) , 𝑓 ∈ ( 𝐾 ‘ 𝑥 ) ↦ ⟨ ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ · ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) , ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ∙ ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) ⟩ ) )

Metamath Proof Explorer

Theorem xpccofval

Proof