Theorem negslem1

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

	Ref	Expression
Assertion	negslem1	⊢ ( 𝐴 = 𝐵 → ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , ◡ 𝑅 ( 𝐴 , 𝐴 ) ↔ ( 𝐹 ↾ 𝐵 ) Isom 𝑅 , ◡ 𝑅 ( 𝐵 , 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 = 𝐵 → 𝐴 = 𝐵 )
2	1 1	resisoeq45d	⊢ ( 𝐴 = 𝐵 → ( ( 𝐹 ↾ 𝐴 ) Isom 𝑅 , ◡ 𝑅 ( 𝐴 , 𝐴 ) ↔ ( 𝐹 ↾ 𝐵 ) Isom 𝑅 , ◡ 𝑅 ( 𝐵 , 𝐵 ) ) )