upcic

Description: A universal property defines an object up to isomorphism given its existence. (Contributed by Zhi Wang, 17-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	upcic	$⊢ φ \to X ≃_{𝑐} (D) Y$

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	simpld	$⊢ φ \to X ≃_{𝑐} (D) Y$

Metamath Proof Explorer