This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ φ → F D Func E G
upcic.x ⊢ φ → X ∈ B
upcic.y ⊢ φ → Y ∈ B
upcic.z ⊢ φ → Z ∈ C
upcic.m ⊢ φ → M ∈ Z J F ⁡ X
upcic.1 ⊢ φ → ∀ w ∈ B ∀ f ∈ Z J F ⁡ w ∃! k ∈ X H w f = X G w ⁡ k Z F ⁡ X O F ⁡ w M
upcic.n ⊢ φ → N ∈ Z J F ⁡ Y
upcic.2 ⊢ φ → ∀ v ∈ B ∀ g ∈ Z J F ⁡ v ∃! l ∈ Y H v g = Y G v ⁡ l Z F ⁡ Y O F ⁡ v N
Assertion upcic ⊢ φ → X ≃ 𝑐 ⁡ D Y

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 ⊢ φ → F D Func E G
7 upcic.x ⊢ φ → X ∈ B
8 upcic.y ⊢ φ → Y ∈ B
9 upcic.z ⊢ φ → Z ∈ C
10 upcic.m ⊢ φ → M ∈ Z J F ⁡ X
11 upcic.1 ⊢ φ → ∀ w ∈ B ∀ f ∈ Z J F ⁡ w ∃! k ∈ X H w f = X G w ⁡ k Z F ⁡ X O F ⁡ w M
12 upcic.n ⊢ φ → N ∈ Z J F ⁡ Y
13 upcic.2 ⊢ φ → ∀ v ∈ B ∀ g ∈ Z J F ⁡ v ∃! l ∈ 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 ⊢ φ → X ≃ 𝑐 ⁡ D Y ∧ ∃ r ∈ X Iso ⁡ D Y N = X G Y ⁡ r Z F ⁡ X O F ⁡ Y M
15 14 simpld ⊢ φ → X ≃ 𝑐 ⁡ D Y