xpchomfval

Description: Set of morphisms of the binary product of categories. (Contributed by Mario Carneiro, 11-Jan-2017) (Proof shortened by AV, 1-Mar-2024)

	Ref	Expression
Hypotheses	xpchomfval.t	⊢ 𝑇 = ( 𝐶 ×_c 𝐷 )
	xpchomfval.y	⊢ 𝐵 = ( Base ‘ 𝑇 )
	xpchomfval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	xpchomfval.j	⊢ 𝐽 = ( Hom ‘ 𝐷 )
	xpchomfval.k	⊢ 𝐾 = ( Hom ‘ 𝑇 )
Assertion	xpchomfval	⊢ 𝐾 = ( 𝑢 ∈ 𝐵 , 𝑣 ∈ 𝐵 ↦ ( ( ( 1^st ‘ 𝑢 ) 𝐻 ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) 𝐽 ( 2^nd ‘ 𝑣 ) ) ) )

Proof

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

Metamath Proof Explorer

Theorem xpchomfval

Proof