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	$⊢ φ \to F (D Func E) G$

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	$⊢ {Base}_{E} = {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 (D Func E) G \leftrightarrow ⟨F, G⟩ \in (D Func E)$
8	7	biimpri	$⊢ ⟨F, G⟩ \in (D Func E) \to F (D Func E) G$
9	1 3 6 8	4syl	$⊢ φ \to F (D Func E) G$

Metamath Proof Explorer