This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 |-