xpcpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same product category. (Contributed by Mario Carneiro, 17-Jan-2017)

	Ref	Expression
Hypotheses	xpcpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
	xpcpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
	xpcpropd.3	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
	xpcpropd.4	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
	xpcpropd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	xpcpropd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	xpcpropd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	xpcpropd.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
Assertion	xpcpropd	⊢ ( 𝜑 → ( 𝐴 ×_c 𝐶 ) = ( 𝐵 ×_c 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		xpcpropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
2		xpcpropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
3		xpcpropd.3	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
4		xpcpropd.4	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
5		xpcpropd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		xpcpropd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
7		xpcpropd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8		xpcpropd.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
9		eqid	⊢ ( 𝐴 ×_c 𝐶 ) = ( 𝐴 ×_c 𝐶 )
10		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
11		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12		eqid	⊢ ( Hom ‘ 𝐴 ) = ( Hom ‘ 𝐴 )
13		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
14		eqid	⊢ ( comp ‘ 𝐴 ) = ( comp ‘ 𝐴 )
15		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
16		eqidd	⊢ ( 𝜑 → ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) = ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) )
17	9 10 11	xpcbas	⊢ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) = ( Base ‘ ( 𝐴 ×_c 𝐶 ) )
18		eqid	⊢ ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) = ( Hom ‘ ( 𝐴 ×_c 𝐶 ) )
19	9 17 12 13 18	xpchomfval	⊢ ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) , 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐴 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑣 ) ) ) )
20	19	a1i	⊢ ( 𝜑 → ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) , 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐴 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑣 ) ) ) ) )
21		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ ) ) = ( 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ ) ) )
22	9 10 11 12 13 14 15 5 7 16 20 21	xpcval	⊢ ( 𝜑 → ( 𝐴 ×_c 𝐶 ) = { ⟨ ( Base ‘ ndx ) , ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ ) ) ⟩ } )
23		eqid	⊢ ( 𝐵 ×_c 𝐷 ) = ( 𝐵 ×_c 𝐷 )
24		eqid	⊢ ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 )
25		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
26		eqid	⊢ ( Hom ‘ 𝐵 ) = ( Hom ‘ 𝐵 )
27		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
28		eqid	⊢ ( comp ‘ 𝐵 ) = ( comp ‘ 𝐵 )
29		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
30	1	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
31	3	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
32	30 31	xpeq12d	⊢ ( 𝜑 → ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) = ( ( Base ‘ 𝐵 ) × ( Base ‘ 𝐷 ) ) )
33	1	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
34		xp1st	⊢ ( 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝑢 ) ∈ ( Base ‘ 𝐴 ) )
35	34	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑢 ) ∈ ( Base ‘ 𝐴 ) )
36		xp1st	⊢ ( 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝑣 ) ∈ ( Base ‘ 𝐴 ) )
37	36	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑣 ) ∈ ( Base ‘ 𝐴 ) )
38	10 12 26 33 35 37	homfeqval	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐴 ) ( 1^st ‘ 𝑣 ) ) = ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐵 ) ( 1^st ‘ 𝑣 ) ) )
39	3	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
40		xp2nd	⊢ ( 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) → ( 2^nd ‘ 𝑢 ) ∈ ( Base ‘ 𝐶 ) )
41	40	3ad2ant2	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( 2^nd ‘ 𝑢 ) ∈ ( Base ‘ 𝐶 ) )
42		xp2nd	⊢ ( 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) → ( 2^nd ‘ 𝑣 ) ∈ ( Base ‘ 𝐶 ) )
43	42	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( 2^nd ‘ 𝑣 ) ∈ ( Base ‘ 𝐶 ) )
44	11 13 27 39 41 43	homfeqval	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑣 ) ) = ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) )
45	38 44	xpeq12d	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ∧ 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐴 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑣 ) ) ) = ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐵 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) )
46	45	mpoeq3dva	⊢ ( 𝜑 → ( 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) , 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐴 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑣 ) ) ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) , 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐵 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) )
47	19 46	syl5eq	⊢ ( 𝜑 → ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) = ( 𝑢 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) , 𝑣 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ↦ ( ( ( 1^st ‘ 𝑢 ) ( Hom ‘ 𝐵 ) ( 1^st ‘ 𝑣 ) ) × ( ( 2^nd ‘ 𝑢 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ) ) )
48	1	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
49	2	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
50		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) )
51		xp1st	⊢ ( 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) )
52	50 51	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 1^st ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) )
53		xp1st	⊢ ( ( 1^st ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐴 ) )
54	52 53	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐴 ) )
55		xp2nd	⊢ ( 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) )
56	50 55	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) )
57		xp1st	⊢ ( ( 2^nd ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) → ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐴 ) )
58	56 57	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐴 ) )
59		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) )
60		xp1st	⊢ ( 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝑦 ) ∈ ( Base ‘ 𝐴 ) )
61	59 60	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 1^st ‘ 𝑦 ) ∈ ( Base ‘ 𝐴 ) )
62		simpr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) )
63		1st2nd2	⊢ ( 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
64	50 63	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
65	64	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) = ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ) )
66		df-ov	⊢ ( ( 1^st ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ( 2^nd ‘ 𝑥 ) ) = ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
67	65 66	eqtr4di	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) = ( ( 1^st ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ( 2^nd ‘ 𝑥 ) ) )
68	9 17 12 13 18 52 56	xpchom	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( ( 1^st ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ( 2^nd ‘ 𝑥 ) ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ) × ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ) ) )
69	67 68	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) = ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ) × ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ) ) )
70	62 69	eleqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → 𝑓 ∈ ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ) × ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ) ) )
71		xp1st	⊢ ( 𝑓 ∈ ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ) × ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ) ) → ( 1^st ‘ 𝑓 ) ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ) )
72	70 71	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 1^st ‘ 𝑓 ) ∈ ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ) )
73		simplr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) )
74	9 17 12 13 18 56 59	xpchom	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) = ( ( ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ 𝑦 ) ) × ( ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) )
75	73 74	eleqtrd	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → 𝑔 ∈ ( ( ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ 𝑦 ) ) × ( ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) )
76		xp1st	⊢ ( 𝑔 ∈ ( ( ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ 𝑦 ) ) × ( ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) → ( 1^st ‘ 𝑔 ) ∈ ( ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ 𝑦 ) ) )
77	75 76	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 1^st ‘ 𝑔 ) ∈ ( ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ 𝑦 ) ) )
78	10 12 14 28 48 49 54 58 61 72 77	comfeqval	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐴 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) = ( ( 1^st ‘ 𝑔 ) ( ⟨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) , ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐵 ) ( 1^st ‘ 𝑦 ) ) ( 1^st ‘ 𝑓 ) ) )
79	3	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
80	4	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
81		xp2nd	⊢ ( ( 1^st ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐶 ) )
82	52 81	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐶 ) )
83		xp2nd	⊢ ( ( 2^nd ‘ 𝑥 ) ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) → ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐶 ) )
84	56 83	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐶 ) )
85		xp2nd	⊢ ( 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) → ( 2^nd ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
86	59 85	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 2^nd ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
87		xp2nd	⊢ ( 𝑓 ∈ ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ) × ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ) ) → ( 2^nd ‘ 𝑓 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ) )
88	70 87	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 2^nd ‘ 𝑓 ) ∈ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ) )
89		xp2nd	⊢ ( 𝑔 ∈ ( ( ( 1^st ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐴 ) ( 1^st ‘ 𝑦 ) ) × ( ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ) → ( 2^nd ‘ 𝑔 ) ∈ ( ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) )
90	75 89	syl	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( 2^nd ‘ 𝑔 ) ∈ ( ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) )
91	11 13 15 29 79 80 82 84 86 88 90	comfeqval	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐶 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) = ( ( 2^nd ‘ 𝑔 ) ( ⟨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐷 ) ( 2^nd ‘ 𝑦 ) ) ( 2^nd ‘ 𝑓 ) ) )
92	78 91	opeq12d	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ = ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ )
93	92	3impa	⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) ∧ 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ) → ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ = ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ )
94	93	mpoeq3dva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 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 ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ ) )
95	94	3impa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) ∧ 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) → ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 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 ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ ) )
96	95	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ ) ) = ( 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ ) ) )
97	23 24 25 26 27 28 29 6 8 32 47 96	xpcval	⊢ ( 𝜑 → ( 𝐵 ×_c 𝐷 ) = { ⟨ ( Base ‘ ndx ) , ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ⟩ , ⟨ ( Hom ‘ ndx ) , ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑥 ∈ ( ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) × ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ) , 𝑦 ∈ ( ( Base ‘ 𝐴 ) × ( Base ‘ 𝐶 ) ) ↦ ( 𝑔 ∈ ( ( 2^nd ‘ 𝑥 ) ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) 𝑦 ) , 𝑓 ∈ ( ( Hom ‘ ( 𝐴 ×_c 𝐶 ) ) ‘ 𝑥 ) ↦ ⟨ ( ( 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 ‘ 𝑓 ) ) ⟩ ) ) ⟩ } )
98	22 97	eqtr4d	⊢ ( 𝜑 → ( 𝐴 ×_c 𝐶 ) = ( 𝐵 ×_c 𝐷 ) )

Metamath Proof Explorer

Theorem xpcpropd

Proof