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

Metamath Proof Explorer

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 𝐸 ) 𝐺 )