Metamath Proof Explorer


Theorem rmyeq

Description: Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014)

Ref Expression
Assertion rmyeq A 2 M N M = N A Y rm M = A Y rm N

Proof

Step Hyp Ref Expression
1 oveq2 a = b A Y rm a = A Y rm b
2 oveq2 a = M A Y rm a = A Y rm M
3 oveq2 a = N A Y rm a = A Y rm N
4 zssre
5 frmy Y rm : 2 ×
6 5 fovcl A 2 a A Y rm a
7 6 zred A 2 a A Y rm a
8 ltrmy A 2 a b a < b A Y rm a < A Y rm b
9 8 biimpd A 2 a b a < b A Y rm a < A Y rm b
10 9 3expb A 2 a b a < b A Y rm a < A Y rm b
11 1 2 3 4 7 10 eqord1 A 2 M N M = N A Y rm M = A Y rm N
12 11 3impb A 2 M N M = N A Y rm M = A Y rm N