Theorem uprcl2

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

	Ref	Expression
Hypothesis	uprcl2.x	|- ( ph -> X ( <. F , G >. ( D UP E ) W ) M )
Assertion	uprcl2	|- ( ph -> F ( D Func E ) G )

Proof

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