Theorem uprcl2

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

	Ref	Expression
Hypothesis	uprcl2.x	⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 )
Assertion	uprcl2	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		uprcl2.x	⊢ ( 𝜑 → 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 )
2		df-br	⊢ ( 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 ↔ ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) )
3	2	biimpi	⊢ ( 𝑋 ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) 𝑀 → ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) )
4		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
5	4	uprcl	⊢ ( ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) ∧ 𝑊 ∈ ( Base ‘ 𝐸 ) ) )
6	5	simpld	⊢ ( ⟨ 𝑋 , 𝑀 ⟩ ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐷 UP 𝐸 ) 𝑊 ) → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
7		df-br	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
8	7	biimpri	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
9	1 3 6 8	4syl	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )