Metamath Proof Explorer


Theorem zextle

Description: An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005)

Ref Expression
Assertion zextle
|- ( ( M e. ZZ /\ N e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> M = N )

Proof

Step Hyp Ref Expression
1 zre
 |-  ( M e. ZZ -> M e. RR )
2 1 leidd
 |-  ( M e. ZZ -> M <_ M )
3 2 adantr
 |-  ( ( M e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> M <_ M )
4 breq1
 |-  ( k = M -> ( k <_ M <-> M <_ M ) )
5 breq1
 |-  ( k = M -> ( k <_ N <-> M <_ N ) )
6 4 5 bibi12d
 |-  ( k = M -> ( ( k <_ M <-> k <_ N ) <-> ( M <_ M <-> M <_ N ) ) )
7 6 rspcva
 |-  ( ( M e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> ( M <_ M <-> M <_ N ) )
8 3 7 mpbid
 |-  ( ( M e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> M <_ N )
9 8 adantlr
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> M <_ N )
10 zre
 |-  ( N e. ZZ -> N e. RR )
11 10 leidd
 |-  ( N e. ZZ -> N <_ N )
12 11 adantr
 |-  ( ( N e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> N <_ N )
13 breq1
 |-  ( k = N -> ( k <_ M <-> N <_ M ) )
14 breq1
 |-  ( k = N -> ( k <_ N <-> N <_ N ) )
15 13 14 bibi12d
 |-  ( k = N -> ( ( k <_ M <-> k <_ N ) <-> ( N <_ M <-> N <_ N ) ) )
16 15 rspcva
 |-  ( ( N e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> ( N <_ M <-> N <_ N ) )
17 12 16 mpbird
 |-  ( ( N e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> N <_ M )
18 17 adantll
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> N <_ M )
19 9 18 jca
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> ( M <_ N /\ N <_ M ) )
20 19 ex
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( A. k e. ZZ ( k <_ M <-> k <_ N ) -> ( M <_ N /\ N <_ M ) ) )
21 letri3
 |-  ( ( M e. RR /\ N e. RR ) -> ( M = N <-> ( M <_ N /\ N <_ M ) ) )
22 1 10 21 syl2an
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M = N <-> ( M <_ N /\ N <_ M ) ) )
23 20 22 sylibrd
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( A. k e. ZZ ( k <_ M <-> k <_ N ) -> M = N ) )
24 23 3impia
 |-  ( ( M e. ZZ /\ N e. ZZ /\ A. k e. ZZ ( k <_ M <-> k <_ N ) ) -> M = N )