Metamath Proof Explorer

Theorem 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 ⊢ 𝐵 = ( 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 upeu ( 𝜑 → ∃! 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )

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 simprd ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
16 eqid ⊢ ( Iso ‘ 𝐷 ) = ( Iso ‘ 𝐷 )
17 6 funcrcl2 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
18 1 3 16 17 7 8 isohom ⊢ ( 𝜑 → ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) )
19 11 8 12 upciclem1 ⊢ ( 𝜑 → ∃! 𝑟 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
20 reurmo ⊢ ( ∃! 𝑟 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) → ∃* 𝑟 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
21 19 20 syl ⊢ ( 𝜑 → ∃* 𝑟 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
22 nfcv ⊢ Ⅎ 𝑟 ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 )
23 nfcv ⊢ Ⅎ 𝑟 ( 𝑋 𝐻 𝑌 )
24 22 23 ssrmof ⊢ ( ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) ⊆ ( 𝑋 𝐻 𝑌 ) → ( ∃* 𝑟 ∈ ( 𝑋 𝐻 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) → ∃* 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
25 18 21 24 sylc ⊢ ( 𝜑 → ∃* 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
26 reu5 ⊢ ( ∃! 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ↔ ( ∃ 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ∧ ∃* 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
27 15 25 26 sylanbrc ⊢ ( 𝜑 → ∃! 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑍 , ( 𝐹 ‘ 𝑋 ) ⟩ 𝑂 ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )