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	$⊢ φ \to G \in (O Func P)$

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	$⊢ {Base}_{P} = {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	$⊢ φ \to (G \in (O Func P) \land W \in {Base}_{P})$
7	6	simpld	$⊢ φ \to G \in (O Func P)$

Metamath Proof Explorer