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 𝐸 ) 𝑊 ) 𝑁 )

Metamath Proof Explorer

Theorem upeu4

Proof