Theorem uobrcl

Description: Reverse closure for universal object. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Assertion	uobrcl	|- ( X e. dom ( F ( D UP E ) W ) -> ( D e. Cat /\ E e. Cat ) )

Proof

Step	Hyp	Ref	Expression
1		eldmg	|- ( X e. dom ( F ( D UP E ) W ) -> ( X e. dom ( F ( D UP E ) W ) <-> E. m X ( F ( D UP E ) W ) m ) )
2	1	ibi	|- ( X e. dom ( F ( D UP E ) W ) -> E. m X ( F ( D UP E ) W ) m )
3		simpr	|- ( ( X e. dom ( F ( D UP E ) W ) /\ X ( F ( D UP E ) W ) m ) -> X ( F ( D UP E ) W ) m )
4	3	up1st2nd	|- ( ( X e. dom ( F ( D UP E ) W ) /\ X ( F ( D UP E ) W ) m ) -> X ( <. ( 1st ` F ) , ( 2nd ` F ) >. ( D UP E ) W ) m )
5	4	uprcl2	|- ( ( X e. dom ( F ( D UP E ) W ) /\ X ( F ( D UP E ) W ) m ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
6	2 5	exlimddv	|- ( X e. dom ( F ( D UP E ) W ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) )
7	6	funcrcl2	|- ( X e. dom ( F ( D UP E ) W ) -> D e. Cat )
8	6	funcrcl3	|- ( X e. dom ( F ( D UP E ) W ) -> E e. Cat )
9	7 8	jca	|- ( X e. dom ( F ( D UP E ) W ) -> ( D e. Cat /\ E e. Cat ) )