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 )