Theorem uobrcl

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

	Ref	Expression
Assertion	uobrcl	Could not format assertion : No typesetting found for |- ( X e. dom ( F ( D UP E ) W ) -> ( D e. Cat /\ E e. Cat ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		eldmg	Could not format ( 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 ) ) : No typesetting found for |- ( 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 ) ) with typecode |-
2	1	ibi	Could not format ( X e. dom ( F ( D UP E ) W ) -> E. m X ( F ( D UP E ) W ) m ) : No typesetting found for |- ( X e. dom ( F ( D UP E ) W ) -> E. m X ( F ( D UP E ) W ) m ) with typecode |-
3		simpr	Could not format ( ( X e. dom ( F ( D UP E ) W ) /\ X ( F ( D UP E ) W ) m ) -> X ( F ( D UP E ) W ) m ) : No typesetting found for |- ( ( X e. dom ( F ( D UP E ) W ) /\ X ( F ( D UP E ) W ) m ) -> X ( F ( D UP E ) W ) m ) with typecode |-
4	3	up1st2nd	Could not format ( ( 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 ) : No typesetting found for |- ( ( 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 ) with typecode |-
5	4	uprcl2	Could not format ( ( X e. dom ( F ( D UP E ) W ) /\ X ( F ( D UP E ) W ) m ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) ) : No typesetting found for |- ( ( X e. dom ( F ( D UP E ) W ) /\ X ( F ( D UP E ) W ) m ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) ) with typecode |-
6	2 5	exlimddv	Could not format ( X e. dom ( F ( D UP E ) W ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) ) : No typesetting found for |- ( X e. dom ( F ( D UP E ) W ) -> ( 1st ` F ) ( D Func E ) ( 2nd ` F ) ) with typecode |-
7	6	funcrcl2	Could not format ( X e. dom ( F ( D UP E ) W ) -> D e. Cat ) : No typesetting found for |- ( X e. dom ( F ( D UP E ) W ) -> D e. Cat ) with typecode |-
8	6	funcrcl3	Could not format ( X e. dom ( F ( D UP E ) W ) -> E e. Cat ) : No typesetting found for |- ( X e. dom ( F ( D UP E ) W ) -> E e. Cat ) with typecode |-
9	7 8	jca	Could not format ( X e. dom ( F ( D UP E ) W ) -> ( D e. Cat /\ E e. Cat ) ) : No typesetting found for |- ( X e. dom ( F ( D UP E ) W ) -> ( D e. Cat /\ E e. Cat ) ) with typecode |-