Metamath Proof Explorer

Theorem upeu3

Description: The universal pair <. X , M >. from object W to functor <. F , G >. is essentially unique (strong form) if it exists. (Contributed by Zhi Wang, 24-Sep-2025)

Ref Expression
Hypotheses upeu3.i ⊢ ( 𝜑 → 𝐼 = ( Iso ‘ 𝐷 ) )
upeu3.o ⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) )
upeu3.x ⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 )
upeu3.y ⊢ ( 𝜑 → 𝑌 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑁 )
Assertion upeu3 ( 𝜑 → ∃! 𝑟 ∈ ( 𝑋 𝐼 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ⚬ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 upeu3.i ⊢ ( 𝜑 → 𝐼 = ( Iso ‘ 𝐷 ) )
2 upeu3.o ⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) )
3 upeu3.x ⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 )
4 upeu3.y ⊢ ( 𝜑 → 𝑌 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑁 )
5 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
6 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
7 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
8 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
9 eqid ⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
10 3 uprcl2 ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
11 3 5 uprcl4 ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
12 4 5 uprcl4 ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
13 3 6 uprcl3 ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐸 ) )
14 3 8 uprcl5 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑊 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
15 5 7 8 9 3 isup2 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∀ 𝑔 ∈ ( 𝑊 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐷 ) 𝑦 ) 𝑔 = ( ( ( 𝑋 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) 𝑀 ) )
16 4 8 uprcl5 ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑊 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) )
17 5 7 8 9 4 isup2 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∀ 𝑔 ∈ ( 𝑊 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) 𝑁 ) )
18 5 6 7 8 9 10 11 12 13 14 15 16 17 upeu ⊢ ( 𝜑 → ∃! 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
19 1 oveqd ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) )
20 2 oveqd ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ⚬ 𝑀 ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
21 20 eqeq2d ⊢ ( 𝜑 → ( 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ⚬ 𝑀 ) ↔ 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
22 19 21 reueqbidv ⊢ ( 𝜑 → ( ∃! 𝑟 ∈ ( 𝑋 𝐼 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ⚬ 𝑀 ) ↔ ∃! 𝑟 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) ) )
23 18 22 mpbird ⊢ ( 𝜑 → ∃! 𝑟 ∈ ( 𝑋 𝐼 𝑌 ) 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑟 ) ⚬ 𝑀 ) )