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

Metamath Proof Explorer

Theorem upeu4

Description: Generate a new universal morphism through an isomorphism from an existing universal object, and pair with the codomain of the isomorphism to form a universal pair. (Contributed by Zhi Wang, 25-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 upeu3.i ⊢ ( 𝜑 → 𝐼 = ( Iso ‘ 𝐷 ) )
2 upeu3.o ⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) )
3 upeu3.x ⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 )
4 upeu4.k ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 𝐼 𝑌 ) )
5 upeu4.n ⊢ ( 𝜑 → 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ⚬ 𝑀 ) )
6 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
7 eqid ⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
8 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9 eqid ⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
10 eqid ⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
11 3 uprcl2 ⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
12 3 6 uprcl4 ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐷 ) )
13 11 funcrcl2 ⊢ ( 𝜑 → 𝐷 ∈ Cat )
14 isofn ⊢ ( 𝐷 ∈ Cat → ( Iso ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
15 13 14 syl ⊢ ( 𝜑 → ( Iso ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
16 1 fneq1d ⊢ ( 𝜑 → ( 𝐼 Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↔ ( Iso ‘ 𝐷 ) Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ) )
17 15 16 mpbird ⊢ ( 𝜑 → 𝐼 Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) )
18 fnov ⊢ ( 𝐼 Fn ( ( Base ‘ 𝐷 ) × ( Base ‘ 𝐷 ) ) ↔ 𝐼 = ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 𝐼 𝑦 ) ) )
19 17 18 sylib ⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 𝐼 𝑦 ) ) )
20 19 oveqd ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = ( 𝑋 ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 𝐼 𝑦 ) ) 𝑌 ) )
21 4 20 eleqtrd ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 𝐼 𝑦 ) ) 𝑌 ) )
22 eqid ⊢ ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 𝐼 𝑦 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 𝐼 𝑦 ) )
23 22 elmpocl2 ⊢ ( 𝐾 ∈ ( 𝑋 ( 𝑥 ∈ ( Base ‘ 𝐷 ) , 𝑦 ∈ ( Base ‘ 𝐷 ) ↦ ( 𝑥 𝐼 𝑦 ) ) 𝑌 ) → 𝑌 ∈ ( Base ‘ 𝐷 ) )
24 21 23 syl ⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝐷 ) )
25 3 7 uprcl3 ⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐸 ) )
26 3 9 uprcl5 ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑊 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
27 6 8 9 10 3 isup2 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐷 ) ∀ 𝑓 ∈ ( 𝑊 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑘 ∈ ( 𝑋 ( Hom ‘ 𝐷 ) 𝑥 ) 𝑓 = ( ( ( 𝑋 𝐺 𝑥 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑥 ) ) 𝑀 ) )
28 eqid ⊢ ( Iso ‘ 𝐷 ) = ( Iso ‘ 𝐷 )
29 1 oveqd ⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) )
30 4 29 eleqtrd ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑋 ( Iso ‘ 𝐷 ) 𝑌 ) )
31 2 oveqd ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ⚬ 𝑀 ) = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
32 5 31 eqtrd ⊢ ( 𝜑 → 𝑁 = ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝐾 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑋 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) 𝑀 ) )
33 6 7 8 9 10 11 12 24 25 26 27 28 30 32 upeu2 ⊢ ( 𝜑 → ( 𝑁 ∈ ( 𝑊 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∀ 𝑔 ∈ ( 𝑊 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) 𝑁 ) ) )
34 33 simprd ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∀ 𝑔 ∈ ( 𝑊 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) 𝑁 ) )
35 33 simpld ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑊 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) )
36 6 7 8 9 10 25 11 24 35 isup ⊢ ( 𝜑 → ( 𝑌 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑁 ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐷 ) ∀ 𝑔 ∈ ( 𝑊 ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) ∃! 𝑘 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑦 ) 𝑔 = ( ( ( 𝑌 𝐺 𝑦 ) ‘ 𝑘 ) ( ⟨ 𝑊 , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑦 ) ) 𝑁 ) ) )
37 34 36 mpbird ⊢ ( 𝜑 → 𝑌 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑁 )