This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iccpartgtl

Description: If there is a partition, then all intermediate points and the upper bound are strictly greater than the lower bound. (Contributed by AV, 14-Jul-2020)

Ref Expression
Hypotheses iccpartgtprec.m 
|- ( ph -> M e. NN )
iccpartgtprec.p 
|- ( ph -> P e. ( RePart ` M ) )
Assertion iccpartgtl 
|- ( ph -> A. i e. ( 1 ... M ) ( P ` 0 ) < ( P ` i ) )

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m 
 |-  ( ph -> M e. NN )
2 iccpartgtprec.p 
 |-  ( ph -> P e. ( RePart ` M ) )
3 elnnuz 
 |-  ( M e. NN <-> M e. ( ZZ>= ` 1 ) )
4 1 3 sylib 
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
5 fzisfzounsn 
 |-  ( M e. ( ZZ>= ` 1 ) -> ( 1 ... M ) = ( ( 1 ..^ M ) u. { M } ) )
6 4 5 syl 
 |-  ( ph -> ( 1 ... M ) = ( ( 1 ..^ M ) u. { M } ) )
7 6 eleq2d 
 |-  ( ph -> ( i e. ( 1 ... M ) <-> i e. ( ( 1 ..^ M ) u. { M } ) ) )
8 elun 
 |-  ( i e. ( ( 1 ..^ M ) u. { M } ) <-> ( i e. ( 1 ..^ M ) \/ i e. { M } ) )
9 8 a1i 
 |-  ( ph -> ( i e. ( ( 1 ..^ M ) u. { M } ) <-> ( i e. ( 1 ..^ M ) \/ i e. { M } ) ) )
10 velsn 
 |-  ( i e. { M } <-> i = M )
11 10 a1i 
 |-  ( ph -> ( i e. { M } <-> i = M ) )
12 11 orbi2d 
 |-  ( ph -> ( ( i e. ( 1 ..^ M ) \/ i e. { M } ) <-> ( i e. ( 1 ..^ M ) \/ i = M ) ) )
13 7 9 12 3bitrd 
 |-  ( ph -> ( i e. ( 1 ... M ) <-> ( i e. ( 1 ..^ M ) \/ i = M ) ) )
14 fveq2 
 |-  ( k = i -> ( P ` k ) = ( P ` i ) )
15 14 breq2d 
 |-  ( k = i -> ( ( P ` 0 ) < ( P ` k ) <-> ( P ` 0 ) < ( P ` i ) ) )
16 15 rspccv 
 |-  ( A. k e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` k ) -> ( i e. ( 1 ..^ M ) -> ( P ` 0 ) < ( P ` i ) ) )
17 1 2 iccpartigtl 
 |-  ( ph -> A. k e. ( 1 ..^ M ) ( P ` 0 ) < ( P ` k ) )
18 16 17 syl11 
 |-  ( i e. ( 1 ..^ M ) -> ( ph -> ( P ` 0 ) < ( P ` i ) ) )
19 1 2 iccpartlt 
 |-  ( ph -> ( P ` 0 ) < ( P ` M ) )
20 19 adantl 
 |-  ( ( i = M /\ ph ) -> ( P ` 0 ) < ( P ` M ) )
21 fveq2 
 |-  ( i = M -> ( P ` i ) = ( P ` M ) )
22 21 adantr 
 |-  ( ( i = M /\ ph ) -> ( P ` i ) = ( P ` M ) )
23 20 22 breqtrrd 
 |-  ( ( i = M /\ ph ) -> ( P ` 0 ) < ( P ` i ) )
24 23 ex 
 |-  ( i = M -> ( ph -> ( P ` 0 ) < ( P ` i ) ) )
25 18 24 jaoi 
 |-  ( ( i e. ( 1 ..^ M ) \/ i = M ) -> ( ph -> ( P ` 0 ) < ( P ` i ) ) )
26 25 com12 
 |-  ( ph -> ( ( i e. ( 1 ..^ M ) \/ i = M ) -> ( P ` 0 ) < ( P ` i ) ) )
27 13 26 sylbid 
 |-  ( ph -> ( i e. ( 1 ... M ) -> ( P ` 0 ) < ( P ` i ) ) )
28 27 ralrimiv 
 |-  ( ph -> A. i e. ( 1 ... M ) ( P ` 0 ) < ( P ` i ) )