upeu

Description: A universal property defines an essentially unique (strong form) pair of object X and morphism M if it exists. (Contributed by Zhi Wang, 19-Sep-2025)

	Ref	Expression
Hypotheses	upcic.b	$⊢ B = {Base}_{D}$
	upcic.c	$⊢ C = {Base}_{E}$
	upcic.h	$⊢ H = Hom (D)$
	upcic.j	$⊢ J = Hom (E)$
	upcic.o	$⊢ O = comp (E)$
	upcic.f	$⊢ φ \to F (D Func E) G$
	upcic.x	$⊢ φ \to X \in B$
	upcic.y	$⊢ φ \to Y \in B$
	upcic.z	$⊢ φ \to Z \in C$
	upcic.m	$⊢ φ \to M \in (Z J F (X))$
	upcic.1	$⊢ φ \to \forall w \in B \forall f \in (Z J F (w)) \exists! k \in (X H w) f = (X G w) (k) (⟨Z, F (X)⟩ O F (w)) M$
	upcic.n	$⊢ φ \to N \in (Z J F (Y))$
	upcic.2	$⊢ φ \to \forall v \in B \forall g \in (Z J F (v)) \exists! l \in (Y H v) g = (Y G v) (l) (⟨Z, F (Y)⟩ O F (v)) N$
Assertion	upeu	$⊢ φ \to \exists! r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M$

Proof

Step	Hyp	Ref	Expression
1		upcic.b	$⊢ B = {Base}_{D}$
2		upcic.c	$⊢ C = {Base}_{E}$
3		upcic.h	$⊢ H = Hom (D)$
4		upcic.j	$⊢ J = Hom (E)$
5		upcic.o	$⊢ O = comp (E)$
6		upcic.f	$⊢ φ \to F (D Func E) G$
7		upcic.x	$⊢ φ \to X \in B$
8		upcic.y	$⊢ φ \to Y \in B$
9		upcic.z	$⊢ φ \to Z \in C$
10		upcic.m	$⊢ φ \to M \in (Z J F (X))$
11		upcic.1	$⊢ φ \to \forall w \in B \forall f \in (Z J F (w)) \exists! k \in (X H w) f = (X G w) (k) (⟨Z, F (X)⟩ O F (w)) M$
12		upcic.n	$⊢ φ \to N \in (Z J F (Y))$
13		upcic.2	$⊢ φ \to \forall v \in B \forall g \in (Z J F (v)) \exists! l \in (Y H v) g = (Y G v) (l) (⟨Z, F (Y)⟩ O F (v)) N$
14	1 2 3 4 5 6 7 8 9 10 11 12 13	upciclem4	$⊢ φ \to (X ≃_{𝑐} (D) Y \land \exists r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M)$
15	14	simprd	$⊢ φ \to \exists r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M$
16		eqid	$⊢ Iso (D) = Iso (D)$
17	6	funcrcl2	$⊢ φ \to D \in Cat$
18	1 3 16 17 7 8	isohom	$⊢ φ \to X Iso (D) Y \subseteq X H Y$
19	11 8 12	upciclem1	$⊢ φ \to \exists! r \in (X H Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M$
20		reurmo	$⊢ \exists! r \in (X H Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M \to \exists^{*} r \in (X H Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M$
21	19 20	syl	$⊢ φ \to \exists^{*} r \in (X H Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M$
22		nfcv	$⊢ \underline{Ⅎ} r (X Iso (D) Y)$
23		nfcv	$⊢ \underline{Ⅎ} r (X H Y)$
24	22 23	ssrmof	$⊢ X Iso (D) Y \subseteq X H Y \to (\exists^{} r \in (X H Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M \to \exists^{} r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M)$
25	18 21 24	sylc	$⊢ φ \to \exists^{*} r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M$
26		reu5	$⊢ \exists! r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M \leftrightarrow (\exists r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M \land \exists^{*} r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M)$
27	15 25 26	sylanbrc	$⊢ φ \to \exists! r \in (X Iso (D) Y) N = (X G Y) (r) (⟨Z, F (X)⟩ O F (Y)) M$

Metamath Proof Explorer

Theorem upeu

Proof