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 φM
iccpartgtprec.p φPRePartM
Assertion iccpartgtl φi1MP0<Pi

Proof

Step Hyp Ref Expression
1 iccpartgtprec.m φM
2 iccpartgtprec.p φPRePartM
3 elnnuz MM1
4 1 3 sylib φM1
5 fzisfzounsn M11M=1..^MM
6 4 5 syl φ1M=1..^MM
7 6 eleq2d φi1Mi1..^MM
8 elun i1..^MMi1..^MiM
9 8 a1i φi1..^MMi1..^MiM
10 velsn iMi=M
11 10 a1i φiMi=M
12 11 orbi2d φi1..^MiMi1..^Mi=M
13 7 9 12 3bitrd φi1Mi1..^Mi=M
14 fveq2 k=iPk=Pi
15 14 breq2d k=iP0<PkP0<Pi
16 15 rspccv k1..^MP0<Pki1..^MP0<Pi
17 1 2 iccpartigtl φk1..^MP0<Pk
18 16 17 syl11 i1..^MφP0<Pi
19 1 2 iccpartlt φP0<PM
20 19 adantl i=MφP0<PM
21 fveq2 i=MPi=PM
22 21 adantr i=MφPi=PM
23 20 22 breqtrrd i=MφP0<Pi
24 23 ex i=MφP0<Pi
25 18 24 jaoi i1..^Mi=MφP0<Pi
26 25 com12 φi1..^Mi=MP0<Pi
27 13 26 sylbid φi1MP0<Pi
28 27 ralrimiv φi1MP0<Pi