Theorem uprcl2a

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

	Ref	Expression
Hypothesis	uprcl2a.x	|- ( ph -> X ( G ( O UP P ) W ) M )
Assertion	uprcl2a	|- ( ph -> G e. ( O Func P ) )

Proof

Step	Hyp	Ref	Expression
1		uprcl2a.x	|- ( ph -> X ( G ( O UP P ) W ) M )
2		df-br	|- ( X ( G ( O UP P ) W ) M <-> <. X , M >. e. ( G ( O UP P ) W ) )
3	1 2	sylib	|- ( ph -> <. X , M >. e. ( G ( O UP P ) W ) )
4		eqid	|- ( Base ` P ) = ( Base ` P )
5	4	uprcl	|- ( <. X , M >. e. ( G ( O UP P ) W ) -> ( G e. ( O Func P ) /\ W e. ( Base ` P ) ) )
6	3 5	syl	|- ( ph -> ( G e. ( O Func P ) /\ W e. ( Base ` P ) ) )
7	6	simpld	|- ( ph -> G e. ( O Func P ) )