Theorem uprcl2a

Description: Reverse closure for the class of universal property. (Contributed by Zhi Wang, 14-Nov-2025)

	Ref	Expression
Hypothesis	uprcl2a.x	⊢ ( 𝜑 → 𝑋 ( 𝐺 ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
Assertion	uprcl2a	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑂 Func 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		uprcl2a.x	⊢ ( 𝜑 → 𝑋 ( 𝐺 ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 )
2		df-br	⊢ ( 𝑋 ( 𝐺 ( 𝑂 UP 𝑃 ) 𝑊 ) 𝑀 ↔ ⟨ 𝑋 , 𝑀 ⟩ ∈ ( 𝐺 ( 𝑂 UP 𝑃 ) 𝑊 ) )
3	1 2	sylib	⊢ ( 𝜑 → ⟨ 𝑋 , 𝑀 ⟩ ∈ ( 𝐺 ( 𝑂 UP 𝑃 ) 𝑊 ) )
4		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
5	4	uprcl	⊢ ( ⟨ 𝑋 , 𝑀 ⟩ ∈ ( 𝐺 ( 𝑂 UP 𝑃 ) 𝑊 ) → ( 𝐺 ∈ ( 𝑂 Func 𝑃 ) ∧ 𝑊 ∈ ( Base ‘ 𝑃 ) ) )
6	3 5	syl	⊢ ( 𝜑 → ( 𝐺 ∈ ( 𝑂 Func 𝑃 ) ∧ 𝑊 ∈ ( Base ‘ 𝑃 ) ) )
7	6	simpld	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑂 Func 𝑃 ) )