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 )