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	$⊢ φ \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
	uppropd.2	$⊢ φ \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
	uppropd.3	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	uppropd.4	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
	uppropd.a	$⊢ φ \to A \in V$
	uppropd.b	$⊢ φ \to B \in V$
	uppropd.c	$⊢ φ \to C \in V$
	uppropd.d	$⊢ φ \to D \in V$
Assertion	uppropd	Could not format assertion : No typesetting found for \|- ( ph -> ( A UP C ) = ( B UP D ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		uppropd.1	$⊢ φ \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
2		uppropd.2	$⊢ φ \to {comp}_{𝑓} (A) = {comp}_{𝑓} (B)$
3		uppropd.3	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
4		uppropd.4	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
5		uppropd.a	$⊢ φ \to A \in V$
6		uppropd.b	$⊢ φ \to B \in V$
7		uppropd.c	$⊢ φ \to C \in V$
8		uppropd.d	$⊢ φ \to D \in V$
9	1 2 3 4 5 6 7 8	funcpropd	$⊢ φ \to A Func C = B Func D$
10	3	homfeqbas	$⊢ φ \to {Base}_{C} = {Base}_{D}$
11	10	adantr	$⊢ (φ \land f \in (A Func C)) \to {Base}_{C} = {Base}_{D}$
12	1	homfeqbas	$⊢ φ \to {Base}_{A} = {Base}_{B}$
13	12	adantr	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to {Base}_{A} = {Base}_{B}$
14	13	adantr	$⊢ ((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \to {Base}_{A} = {Base}_{B}$
15		eqid	$⊢ {Base}_{C} = {Base}_{C}$
16		eqid	$⊢ Hom (C) = Hom (C)$
17		eqid	$⊢ Hom (D) = Hom (D)$
18	3	ad3antrrr	$⊢ (((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
19		simprr	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to w \in {Base}_{C}$
20	19	ad2antrr	$⊢ (((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \to w \in {Base}_{C}$
21		eqid	$⊢ {Base}_{A} = {Base}_{A}$
22		simprl	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to f \in (A Func C)$
23	22	func1st2nd	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to 1^{st} (f) (A Func C) 2^{nd} (f)$
24	21 15 23	funcf1	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to 1^{st} (f) : {Base}_{A} ⟶ {Base}_{C}$
25	24	adantr	$⊢ ((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \to 1^{st} (f) : {Base}_{A} ⟶ {Base}_{C}$
26	25	ffvelcdmda	$⊢ (((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \to 1^{st} (f) (y) \in {Base}_{C}$
27	15 16 17 18 20 26	homfeqval	$⊢ (((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \to w Hom (C) 1^{st} (f) (y) = w Hom (D) 1^{st} (f) (y)$
28		eqid	$⊢ Hom (A) = Hom (A)$
29		eqid	$⊢ Hom (B) = Hom (B)$
30	1	ad4antr	$⊢ ((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \to {Hom}_{𝑓} (A) = {Hom}_{𝑓} (B)$
31		simprl	$⊢ ((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \to x \in {Base}_{A}$
32	31	ad2antrr	$⊢ ((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \to x \in {Base}_{A}$
33		simplr	$⊢ ((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \to y \in {Base}_{A}$
34	21 28 29 30 32 33	homfeqval	$⊢ ((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \to x Hom (A) y = x Hom (B) y$
35		eqid	$⊢ comp (C) = comp (C)$
36		eqid	$⊢ comp (D) = comp (D)$
37	18	ad2antrr	$⊢ (((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \land k \in (x Hom (A) y)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
38	4	ad5antr	$⊢ (((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \land k \in (x Hom (A) y)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
39	20	ad2antrr	$⊢ (((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \land k \in (x Hom (A) y)) \to w \in {Base}_{C}$
40	24	ffvelcdmda	$⊢ ((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land x \in {Base}_{A}) \to 1^{st} (f) (x) \in {Base}_{C}$
41	40	adantrr	$⊢ ((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \to 1^{st} (f) (x) \in {Base}_{C}$
42	41	ad3antrrr	$⊢ (((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \land k \in (x Hom (A) y)) \to 1^{st} (f) (x) \in {Base}_{C}$
43	26	ad2antrr	$⊢ (((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \land k \in (x Hom (A) y)) \to 1^{st} (f) (y) \in {Base}_{C}$
44		simprr	$⊢ ((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \to m \in (w Hom (C) 1^{st} (f) (x))$
45	44	ad3antrrr	$⊢ (((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \land k \in (x Hom (A) y)) \to m \in (w Hom (C) 1^{st} (f) (x))$
46	23	ad3antrrr	$⊢ ((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \to 1^{st} (f) (A Func C) 2^{nd} (f)$
47	21 28 16 46 32 33	funcf2	$⊢ ((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \to (x 2^{nd} (f) y) : x Hom (A) y ⟶ 1^{st} (f) (x) Hom (C) 1^{st} (f) (y)$
48	47	ffvelcdmda	$⊢ (((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \land k \in (x Hom (A) y)) \to (x 2^{nd} (f) y) (k) \in (1^{st} (f) (x) Hom (C) 1^{st} (f) (y))$
49	15 16 35 36 37 38 39 42 43 45 48	comfeqval	$⊢ (((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \land k \in (x Hom (A) y)) \to (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (C) 1^{st} (f) (y)) m = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (D) 1^{st} (f) (y)) m$
50	49	eqeq2d	$⊢ (((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \land k \in (x Hom (A) y)) \to (g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (C) 1^{st} (f) (y)) m \leftrightarrow g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (D) 1^{st} (f) (y)) m)$
51	34 50	reueqbidva	$⊢ ((((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \land g \in (w Hom (C) 1^{st} (f) (y))) \to (\exists! k \in (x Hom (A) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (C) 1^{st} (f) (y)) m \leftrightarrow \exists! k \in (x Hom (B) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (D) 1^{st} (f) (y)) m)$
52	27 51	raleqbidva	$⊢ (((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \land y \in {Base}_{A}) \to (\forall g \in (w Hom (C) 1^{st} (f) (y)) \exists! k \in (x Hom (A) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (C) 1^{st} (f) (y)) m \leftrightarrow \forall g \in (w Hom (D) 1^{st} (f) (y)) \exists! k \in (x Hom (B) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (D) 1^{st} (f) (y)) m)$
53	14 52	raleqbidva	$⊢ ((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land (x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x)))) \to (\forall y \in {Base}_{A} \forall g \in (w Hom (C) 1^{st} (f) (y)) \exists! k \in (x Hom (A) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (C) 1^{st} (f) (y)) m \leftrightarrow \forall y \in {Base}_{B} \forall g \in (w Hom (D) 1^{st} (f) (y)) \exists! k \in (x Hom (B) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (D) 1^{st} (f) (y)) m)$
54	53	pm5.32da	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to (((x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x))) \land \forall y \in {Base}_{A} \forall g \in (w Hom (C) 1^{st} (f) (y)) \exists! k \in (x Hom (A) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (C) 1^{st} (f) (y)) m) \leftrightarrow ((x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x))) \land \forall y \in {Base}_{B} \forall g \in (w Hom (D) 1^{st} (f) (y)) \exists! k \in (x Hom (B) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (D) 1^{st} (f) (y)) m))$
55	3	ad2antrr	$⊢ ((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land x \in {Base}_{A}) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
56		simplrr	$⊢ ((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land x \in {Base}_{A}) \to w \in {Base}_{C}$
57	15 16 17 55 56 40	homfeqval	$⊢ ((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land x \in {Base}_{A}) \to w Hom (C) 1^{st} (f) (x) = w Hom (D) 1^{st} (f) (x)$
58	57	eleq2d	$⊢ ((φ \land (f \in (A Func C) \land w \in {Base}_{C})) \land x \in {Base}_{A}) \to (m \in (w Hom (C) 1^{st} (f) (x)) \leftrightarrow m \in (w Hom (D) 1^{st} (f) (x)))$
59	58	pm5.32da	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to ((x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x))) \leftrightarrow (x \in {Base}_{A} \land m \in (w Hom (D) 1^{st} (f) (x))))$
60	13	eleq2d	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to (x \in {Base}_{A} \leftrightarrow x \in {Base}_{B})$
61	60	anbi1d	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to ((x \in {Base}_{A} \land m \in (w Hom (D) 1^{st} (f) (x))) \leftrightarrow (x \in {Base}_{B} \land m \in (w Hom (D) 1^{st} (f) (x))))$
62	59 61	bitrd	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to ((x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x))) \leftrightarrow (x \in {Base}_{B} \land m \in (w Hom (D) 1^{st} (f) (x))))$
63	62	anbi1d	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to (((x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x))) \land \forall y \in {Base}_{B} \forall g \in (w Hom (D) 1^{st} (f) (y)) \exists! k \in (x Hom (B) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (D) 1^{st} (f) (y)) m) \leftrightarrow ((x \in {Base}_{B} \land m \in (w Hom (D) 1^{st} (f) (x))) \land \forall y \in {Base}_{B} \forall g \in (w Hom (D) 1^{st} (f) (y)) \exists! k \in (x Hom (B) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (D) 1^{st} (f) (y)) m))$
64	54 63	bitrd	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to (((x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x))) \land \forall y \in {Base}_{A} \forall g \in (w Hom (C) 1^{st} (f) (y)) \exists! k \in (x Hom (A) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (C) 1^{st} (f) (y)) m) \leftrightarrow ((x \in {Base}_{B} \land m \in (w Hom (D) 1^{st} (f) (x))) \land \forall y \in {Base}_{B} \forall g \in (w Hom (D) 1^{st} (f) (y)) \exists! k \in (x Hom (B) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (D) 1^{st} (f) (y)) m))$
65	64	opabbidv	$⊢ (φ \land (f \in (A Func C) \land w \in {Base}_{C})) \to \{⟨x, m⟩ \| ((x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x))) \land \forall y \in {Base}_{A} \forall g \in (w Hom (C) 1^{st} (f) (y)) \exists! k \in (x Hom (A) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (C) 1^{st} (f) (y)) m)\} = \{⟨x, m⟩ \| ((x \in {Base}_{B} \land m \in (w Hom (D) 1^{st} (f) (x))) \land \forall y \in {Base}_{B} \forall g \in (w Hom (D) 1^{st} (f) (y)) \exists! k \in (x Hom (B) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (D) 1^{st} (f) (y)) m)\}$
66	9 11 65	mpoeq123dva	$⊢ φ \to (f \in (A Func C), w \in {Base}_{C} ⟼ \{⟨x, m⟩ \| ((x \in {Base}_{A} \land m \in (w Hom (C) 1^{st} (f) (x))) \land \forall y \in {Base}_{A} \forall g \in (w Hom (C) 1^{st} (f) (y)) \exists! k \in (x Hom (A) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (C) 1^{st} (f) (y)) m)\}) = (f \in (B Func D), w \in {Base}_{D} ⟼ \{⟨x, m⟩ \| ((x \in {Base}_{B} \land m \in (w Hom (D) 1^{st} (f) (x))) \land \forall y \in {Base}_{B} \forall g \in (w Hom (D) 1^{st} (f) (y)) \exists! k \in (x Hom (B) y) g = (x 2^{nd} (f) y) (k) (⟨w, 1^{st} (f) (x)⟩ comp (D) 1^{st} (f) (y)) m)\})$
67	21 15 28 16 35	upfval	Could not format ( A UP C ) = ( f e. ( A Func C ) , w e. ( Base ` C ) \|-> { <. x , m >. \| ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` A ) A. g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` A ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) ) } ) : No typesetting found for \|- ( A UP C ) = ( f e. ( A Func C ) , w e. ( Base ` C ) \|-> { <. x , m >. \| ( ( x e. ( Base ` A ) /\ m e. ( w ( Hom ` C ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` A ) A. g e. ( w ( Hom ` C ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` A ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` C ) ( ( 1st ` f ) ` y ) ) m ) ) } ) with typecode \|-
68		eqid	$⊢ {Base}_{B} = {Base}_{B}$
69		eqid	$⊢ {Base}_{D} = {Base}_{D}$
70	68 69 29 17 36	upfval	Could not format ( B UP D ) = ( f e. ( B Func D ) , w e. ( Base ` D ) \|-> { <. x , m >. \| ( ( x e. ( Base ` B ) /\ m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` B ) A. g e. ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) } ) : No typesetting found for \|- ( B UP D ) = ( f e. ( B Func D ) , w e. ( Base ` D ) \|-> { <. x , m >. \| ( ( x e. ( Base ` B ) /\ m e. ( w ( Hom ` D ) ( ( 1st ` f ) ` x ) ) ) /\ A. y e. ( Base ` B ) A. g e. ( w ( Hom ` D ) ( ( 1st ` f ) ` y ) ) E! k e. ( x ( Hom ` B ) y ) g = ( ( ( x ( 2nd ` f ) y ) ` k ) ( <. w , ( ( 1st ` f ) ` x ) >. ( comp ` D ) ( ( 1st ` f ) ` y ) ) m ) ) } ) with typecode \|-
71	66 67 70	3eqtr4g	Could not format ( ph -> ( A UP C ) = ( B UP D ) ) : No typesetting found for \|- ( ph -> ( A UP C ) = ( B UP D ) ) with typecode \|-

Metamath Proof Explorer

Theorem uppropd

Proof