Theorem uprcl2a

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

	Ref	Expression
Hypothesis	uprcl2a.x	No typesetting found for |- ( ph -> X ( G ( O UP P ) W ) M ) with typecode |-
Assertion	uprcl2a	$$⊢\phi \to G\in \left(O\mathrm{Func}P\right)$$

Proof

Step	Hyp	Ref	Expression
1		uprcl2a.x	Could not format ( ph -> X ( G ( O UP P ) W ) M ) : No typesetting found for |- ( ph -> X ( G ( O UP P ) W ) M ) with typecode |-
2		df-br	Could not format ( X ( G ( O UP P ) W ) M <-> <. X , M >. e. ( G ( O UP P ) W ) ) : No typesetting found for |- ( X ( G ( O UP P ) W ) M <-> <. X , M >. e. ( G ( O UP P ) W ) ) with typecode |-
3	1 2	sylib	Could not format ( ph -> <. X , M >. e. ( G ( O UP P ) W ) ) : No typesetting found for |- ( ph -> <. X , M >. e. ( G ( O UP P ) W ) ) with typecode |-
4		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
5	4	uprcl	Could not format ( <. X , M >. e. ( G ( O UP P ) W ) -> ( G e. ( O Func P ) /\ W e. ( Base ` P ) ) ) : No typesetting found for |- ( <. X , M >. e. ( G ( O UP P ) W ) -> ( G e. ( O Func P ) /\ W e. ( Base ` P ) ) ) with typecode |-
6	3 5	syl	$$⊢\phi \to \left(G\in \left(O\mathrm{Func}P\right)\wedge W\in {\mathrm{Base}}_P\right)$$
7	6	simpld	$$⊢\phi \to G\in \left(O\mathrm{Func}P\right)$$