Theorem 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={\mathrm{Base}}_E$$
Assertion	uprcl3	$$⊢\phi \to W\in C$$

Proof

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={\mathrm{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	$$⊢\phi \to W\in C$$