Theorem uprcl2

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

	Ref	Expression
Hypothesis	uprcl2.x	No typesetting found for |- ( ph -> X ( <. F , G >. ( D UP E ) W ) M ) with typecode |-
Assertion	uprcl2	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$

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		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 |-
3	2	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 |-
4		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
5	4	uprcl	Could not format ( <. X , M >. e. ( <. F , G >. ( D UP E ) W ) -> ( <. F , G >. e. ( D Func E ) /\ W e. ( Base ` E ) ) ) : No typesetting found for |- ( <. X , M >. e. ( <. F , G >. ( D UP E ) W ) -> ( <. F , G >. e. ( D Func E ) /\ W e. ( Base ` E ) ) ) with typecode |-
6	5	simpld	Could not format ( <. X , M >. e. ( <. F , G >. ( D UP E ) W ) -> <. F , G >. e. ( D Func E ) ) : No typesetting found for |- ( <. X , M >. e. ( <. F , G >. ( D UP E ) W ) -> <. F , G >. e. ( D Func E ) ) with typecode |-
7		df-br	$$⊢F\left(D\mathrm{Func}E\right)G\leftrightarrow ⟨F,G⟩\in \left(D\mathrm{Func}E\right)$$
8	7	biimpri	$$⊢⟨F,G⟩\in \left(D\mathrm{Func}E\right)\to F\left(D\mathrm{Func}E\right)G$$
9	1 3 6 8	4syl	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$