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	⊢ 𝐵 = ( Base ‘ 𝐷 )
	upcic.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
	upcic.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
	upcic.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
	upcic.o	⊢ 𝑂 = ( comp ‘ 𝐸 )
	upcic.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
	upcic.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	upcic.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	upcic.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐶 )
	upcic.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
	upcic.1	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑤 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) 𝑓 = ( ( ( 𝑋 𝐺 𝑤 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑤 ) ) 𝑀 ) )
	upcic.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
	upcic.2	⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ∃! 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) )
Assertion	upcic	⊢ ( 𝜑 → 𝑋 ( ≃𝑐 ‘ 𝐷 ) 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		upcic.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		upcic.c	⊢ 𝐶 = ( Base ‘ 𝐸 )
3		upcic.h	⊢ 𝐻 = ( Hom ‘ 𝐷 )
4		upcic.j	⊢ 𝐽 = ( Hom ‘ 𝐸 )
5		upcic.o	⊢ 𝑂 = ( comp ‘ 𝐸 )
6		upcic.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
7		upcic.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		upcic.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		upcic.z	⊢ ( 𝜑 → 𝑍 ∈ 𝐶 )
10		upcic.m	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑋 ) ) )
11		upcic.1	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝐵 ∀ 𝑓 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑤 ) ) ∃! 𝑘 ∈ ( 𝑋 𝐻 𝑤 ) 𝑓 = ( ( ( 𝑋 𝐺 𝑤 ) ‘ 𝑘 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑤 ) ) 𝑀 ) )
12		upcic.n	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑌 ) ) )
13		upcic.2	⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑍 𝐽 ( 𝐹 ‘ 𝑣 ) ) ∃! 𝑙 ∈ ( 𝑌 𝐻 𝑣 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑣 ) ‘ 𝑙 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑌 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑣 ) ) 𝑁 ) )
14	1 2 3 4 5 6 7 8 9 10 11 12 13	upciclem4	⊢ ( 𝜑 → ( 𝑋 ( ≃𝑐 ‘ 𝐷 ) 𝑌 ∧ ∃ 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
15	14	simpld	⊢ ( 𝜑 → 𝑋 ( ≃𝑐 ‘ 𝐷 ) 𝑌 )