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

Metamath Proof Explorer

Theorem uprcl3

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

Ref Expression
Hypotheses uprcl2.x 
|- ( ph -> X ( <. F , G >. ( D UP E ) W ) M )
uprcl3.c 
|- C = ( Base ` E )
Assertion uprcl3 
|- ( ph -> W e. C )

Proof

Step Hyp Ref Expression
1 uprcl2.x 
 |-  ( ph -> X ( <. F , G >. ( D UP E ) W ) M )
2 uprcl3.c 
 |-  C = ( Base ` E )
3 df-br 
 |-  ( X ( <. F , G >. ( D UP E ) W ) M <-> <. X , M >. e. ( <. F , G >. ( D UP E ) W ) )
4 3 biimpi 
 |-  ( X ( <. F , G >. ( D UP E ) W ) M -> <. X , M >. e. ( <. F , G >. ( D UP E ) W ) )
5 2 uprcl 
 |-  ( <. X , M >. e. ( <. F , G >. ( D UP E ) W ) -> ( <. F , G >. e. ( D Func E ) /\ W e. C ) )
6 5 simprd 
 |-  ( <. X , M >. e. ( <. F , G >. ( D UP E ) W ) -> W e. C )
7 1 4 6 3syl 
 |-  ( ph -> W e. C )