uppropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same universal pairs. (Contributed by Zhi Wang, 20-Nov-2025)

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

Proof

Step	Hyp	Ref	Expression
1		uppropd.1	⊢ ( 𝜑 → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
2		uppropd.2	⊢ ( 𝜑 → ( comp_f ‘ 𝐴 ) = ( comp_f ‘ 𝐵 ) )
3		uppropd.3	⊢ ( 𝜑 → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
4		uppropd.4	⊢ ( 𝜑 → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
5		uppropd.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6		uppropd.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
7		uppropd.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8		uppropd.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
9	1 2 3 4 5 6 7 8	funcpropd	⊢ ( 𝜑 → ( 𝐴 Func 𝐶 ) = ( 𝐵 Func 𝐷 ) )
10	3	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐴 Func 𝐶 ) ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
12	1	homfeqbas	⊢ ( 𝜑 → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
13	12	adantr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
14	13	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) → ( Base ‘ 𝐴 ) = ( Base ‘ 𝐵 ) )
15		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
16		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
17		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
18	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
19		simprr	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
20	19	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
21		eqid	⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
22		simprl	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → 𝑓 ∈ ( 𝐴 Func 𝐶 ) )
23	22	func1st2nd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑓 ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑓 ) )
24	21 15 23	funcf1	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → ( 1^st ‘ 𝑓 ) : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
25	24	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) → ( 1^st ‘ 𝑓 ) : ( Base ‘ 𝐴 ) ⟶ ( Base ‘ 𝐶 ) )
26	25	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
27	15 16 17 18 20 26	homfeqval	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) = ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) )
28		eqid	⊢ ( Hom ‘ 𝐴 ) = ( Hom ‘ 𝐴 )
29		eqid	⊢ ( Hom ‘ 𝐵 ) = ( Hom ‘ 𝐵 )
30	1	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) → ( Hom_f ‘ 𝐴 ) = ( Hom_f ‘ 𝐵 ) )
31		simprl	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
32	31	ad2antrr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
33		simplr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
34	21 28 29 30 32 33	homfeqval	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) → ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) )
35		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
36		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
37	18	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
38	4	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( comp_f ‘ 𝐶 ) = ( comp_f ‘ 𝐷 ) )
39	20	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
40	24	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
41	40	adantrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
42	41	ad3antrrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
43	26	ad2antrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ∈ ( Base ‘ 𝐶 ) )
44		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) → 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) )
45	44	ad3antrrr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) )
46	23	ad3antrrr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) → ( 1^st ‘ 𝑓 ) ( 𝐴 Func 𝐶 ) ( 2^nd ‘ 𝑓 ) )
47	21 28 16 46 32 33	funcf2	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) → ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) : ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ⟶ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) )
48	47	ffvelcdmda	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ∈ ( ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) )
49	15 16 35 36 37 38 39 42 43 45 48	comfeqval	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) )
50	49	eqeq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) ∧ 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) ) → ( 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) )
51	34 50	reueqbidva	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) ∧ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ) → ( ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) )
52	27 51	raleqbidva	⊢ ( ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝐴 ) ) → ( ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) )
53	14 52	raleqbidva	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) )
54	53	pm5.32da	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) ) )
55	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( Hom_f ‘ 𝐶 ) = ( Hom_f ‘ 𝐷 ) )
56		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → 𝑤 ∈ ( Base ‘ 𝐶 ) )
57	15 16 17 55 56 40	homfeqval	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) = ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) )
58	57	eleq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐴 ) ) → ( 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ↔ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) )
59	58	pm5.32da	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) )
60	13	eleq2d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → ( 𝑥 ∈ ( Base ‘ 𝐴 ) ↔ 𝑥 ∈ ( Base ‘ 𝐵 ) ) )
61	60	anbi1d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) )
62	59 61	bitrd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ↔ ( 𝑥 ∈ ( Base ‘ 𝐵 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ) )
63	62	anbi1d	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐵 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) ) )
64	54 63	bitrd	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → ( ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) ↔ ( ( 𝑥 ∈ ( Base ‘ 𝐵 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) ) )
65	64	opabbidv	⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) ∧ 𝑤 ∈ ( Base ‘ 𝐶 ) ) ) → { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } = { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐵 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } )
66	9 11 65	mpoeq123dva	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) = ( 𝑓 ∈ ( 𝐵 Func 𝐷 ) , 𝑤 ∈ ( Base ‘ 𝐷 ) ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐵 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } ) )
67	21 15 28 16 35	upfval	⊢ ( 𝐴 UP 𝐶 ) = ( 𝑓 ∈ ( 𝐴 Func 𝐶 ) , 𝑤 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐴 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐴 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐴 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐶 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } )
68		eqid	⊢ ( Base ‘ 𝐵 ) = ( Base ‘ 𝐵 )
69		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
70	68 69 29 17 36	upfval	⊢ ( 𝐵 UP 𝐷 ) = ( 𝑓 ∈ ( 𝐵 Func 𝐷 ) , 𝑤 ∈ ( Base ‘ 𝐷 ) ↦ { ⟨ 𝑥 , 𝑚 ⟩ ∣ ( ( 𝑥 ∈ ( Base ‘ 𝐵 ) ∧ 𝑚 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐵 ) ∀ 𝑔 ∈ ( 𝑤 ( Hom ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑥 ( Hom ‘ 𝐵 ) 𝑦 ) 𝑔 = ( ( ( 𝑥 ( 2^nd ‘ 𝑓 ) 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑤 , ( ( 1^st ‘ 𝑓 ) ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( ( 1^st ‘ 𝑓 ) ‘ 𝑦 ) ) 𝑚 ) ) } )
71	66 67 70	3eqtr4g	⊢ ( 𝜑 → ( 𝐴 UP 𝐶 ) = ( 𝐵 UP 𝐷 ) )

Metamath Proof Explorer

Theorem uppropd

Proof