uprcl3

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

	Ref	Expression
Hypotheses	uprcl2.x	No typesetting found for \|- ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) with typecode \|-
	uprcl3.c	$⊢ C = {Base}_{E}$
Assertion	uprcl3	$⊢ φ \to W \in C$

Step	Hyp	Ref	Expression
1		uprcl2.x	Could not format ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) : No typesetting found for \|- ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) with typecode \|-
2		uprcl3.c	$⊢ C = {Base}_{E}$
3		df-br	Could not format ( X ( <. F , G >. ( D UP E ) W ) M <-> <. X , M >. e. ( <. F , G >. ( D UP E ) W ) ) : No typesetting found for \|- ( X ( <. F , G >. ( D UP E ) W ) M <-> <. X , M >. e. ( <. F , G >. ( D UP E ) W ) ) with typecode \|-
4	3	biimpi	Could not format ( X ( <. F , G >. ( D UP E ) W ) M -> <. X , M >. e. ( <. F , G >. ( D UP E ) W ) ) : No typesetting found for \|- ( X ( <. F , G >. ( D UP E ) W ) M -> <. X , M >. e. ( <. F , G >. ( D UP E ) W ) ) with typecode \|-
5	2	uprcl	Could not format ( <. X , M >. e. ( <. F , G >. ( D UP E ) W ) -> ( <. F , G >. e. ( D Func E ) /\ W e. C ) ) : No typesetting found for \|- ( <. X , M >. e. ( <. F , G >. ( D UP E ) W ) -> ( <. F , G >. e. ( D Func E ) /\ W e. C ) ) with typecode \|-
6	5	simprd	Could not format ( <. X , M >. e. ( <. F , G >. ( D UP E ) W ) -> W e. C ) : No typesetting found for \|- ( <. X , M >. e. ( <. F , G >. ( D UP E ) W ) -> W e. C ) with typecode \|-
7	1 4 6	3syl	$⊢ φ \to W \in C$

Metamath Proof Explorer