Metamath Proof Explorer

Theorem negslem1

Description: An equivalence between identically restricted order-reversing self-isometries. (Contributed by RP, 30-Sep-2024)

Ref Expression
Assertion negslem1 
|- ( A = B -> ( ( F |` A ) Isom R , `' R ( A , A ) <-> ( F |` B ) Isom R , `' R ( B , B ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A = B -> A = B )
2 1 1 resisoeq45d 
 |-  ( A = B -> ( ( F |` A ) Isom R , `' R ( A , A ) <-> ( F |` B ) Isom R , `' R ( B , B ) ) )