Metamath Proof Explorer

Theorem pmltpclem1

Description: Lemma for pmltpc . (Contributed by Mario Carneiro, 1-Jul-2014)

Ref Expression
Hypotheses pmltpclem1.1 
|- ( ph -> A e. S )
pmltpclem1.2 
|- ( ph -> B e. S )
pmltpclem1.3 
|- ( ph -> C e. S )
pmltpclem1.4 
|- ( ph -> A < B )
pmltpclem1.5 
|- ( ph -> B < C )
pmltpclem1.6 
|- ( ph -> ( ( ( F ` A ) < ( F ` B ) /\ ( F ` C ) < ( F ` B ) ) \/ ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` C ) ) ) )
Assertion pmltpclem1 
|- ( ph -> E. a e. S E. b e. S E. c e. S ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmltpclem1.1 
 |-  ( ph -> A e. S )
2 pmltpclem1.2 
 |-  ( ph -> B e. S )
3 pmltpclem1.3 
 |-  ( ph -> C e. S )
4 pmltpclem1.4 
 |-  ( ph -> A < B )
5 pmltpclem1.5 
 |-  ( ph -> B < C )
6 pmltpclem1.6 
 |-  ( ph -> ( ( ( F ` A ) < ( F ` B ) /\ ( F ` C ) < ( F ` B ) ) \/ ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` C ) ) ) )
7 breq1 
 |-  ( a = A -> ( a < b <-> A < b ) )
8 fveq2 
 |-  ( a = A -> ( F ` a ) = ( F ` A ) )
9 8 breq1d 
 |-  ( a = A -> ( ( F ` a ) < ( F ` b ) <-> ( F ` A ) < ( F ` b ) ) )
10 9 anbi1d 
 |-  ( a = A -> ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) <-> ( ( F ` A ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) ) )
11 8 breq2d 
 |-  ( a = A -> ( ( F ` b ) < ( F ` a ) <-> ( F ` b ) < ( F ` A ) ) )
12 11 anbi1d 
 |-  ( a = A -> ( ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) <-> ( ( F ` b ) < ( F ` A ) /\ ( F ` b ) < ( F ` c ) ) ) )
13 10 12 orbi12d 
 |-  ( a = A -> ( ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) <-> ( ( ( F ` A ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` A ) /\ ( F ` b ) < ( F ` c ) ) ) ) )
14 7 13 3anbi13d 
 |-  ( a = A -> ( ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) <-> ( A < b /\ b < c /\ ( ( ( F ` A ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` A ) /\ ( F ` b ) < ( F ` c ) ) ) ) ) )
15 breq2 
 |-  ( b = B -> ( A < b <-> A < B ) )
16 breq1 
 |-  ( b = B -> ( b < c <-> B < c ) )
17 fveq2 
 |-  ( b = B -> ( F ` b ) = ( F ` B ) )
18 17 breq2d 
 |-  ( b = B -> ( ( F ` A ) < ( F ` b ) <-> ( F ` A ) < ( F ` B ) ) )
19 17 breq2d 
 |-  ( b = B -> ( ( F ` c ) < ( F ` b ) <-> ( F ` c ) < ( F ` B ) ) )
20 18 19 anbi12d 
 |-  ( b = B -> ( ( ( F ` A ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) <-> ( ( F ` A ) < ( F ` B ) /\ ( F ` c ) < ( F ` B ) ) ) )
21 17 breq1d 
 |-  ( b = B -> ( ( F ` b ) < ( F ` A ) <-> ( F ` B ) < ( F ` A ) ) )
22 17 breq1d 
 |-  ( b = B -> ( ( F ` b ) < ( F ` c ) <-> ( F ` B ) < ( F ` c ) ) )
23 21 22 anbi12d 
 |-  ( b = B -> ( ( ( F ` b ) < ( F ` A ) /\ ( F ` b ) < ( F ` c ) ) <-> ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` c ) ) ) )
24 20 23 orbi12d 
 |-  ( b = B -> ( ( ( ( F ` A ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` A ) /\ ( F ` b ) < ( F ` c ) ) ) <-> ( ( ( F ` A ) < ( F ` B ) /\ ( F ` c ) < ( F ` B ) ) \/ ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` c ) ) ) ) )
25 15 16 24 3anbi123d 
 |-  ( b = B -> ( ( A < b /\ b < c /\ ( ( ( F ` A ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` A ) /\ ( F ` b ) < ( F ` c ) ) ) ) <-> ( A < B /\ B < c /\ ( ( ( F ` A ) < ( F ` B ) /\ ( F ` c ) < ( F ` B ) ) \/ ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` c ) ) ) ) ) )
26 breq2 
 |-  ( c = C -> ( B < c <-> B < C ) )
27 fveq2 
 |-  ( c = C -> ( F ` c ) = ( F ` C ) )
28 27 breq1d 
 |-  ( c = C -> ( ( F ` c ) < ( F ` B ) <-> ( F ` C ) < ( F ` B ) ) )
29 28 anbi2d 
 |-  ( c = C -> ( ( ( F ` A ) < ( F ` B ) /\ ( F ` c ) < ( F ` B ) ) <-> ( ( F ` A ) < ( F ` B ) /\ ( F ` C ) < ( F ` B ) ) ) )
30 27 breq2d 
 |-  ( c = C -> ( ( F ` B ) < ( F ` c ) <-> ( F ` B ) < ( F ` C ) ) )
31 30 anbi2d 
 |-  ( c = C -> ( ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` c ) ) <-> ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` C ) ) ) )
32 29 31 orbi12d 
 |-  ( c = C -> ( ( ( ( F ` A ) < ( F ` B ) /\ ( F ` c ) < ( F ` B ) ) \/ ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` c ) ) ) <-> ( ( ( F ` A ) < ( F ` B ) /\ ( F ` C ) < ( F ` B ) ) \/ ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` C ) ) ) ) )
33 26 32 3anbi23d 
 |-  ( c = C -> ( ( A < B /\ B < c /\ ( ( ( F ` A ) < ( F ` B ) /\ ( F ` c ) < ( F ` B ) ) \/ ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` c ) ) ) ) <-> ( A < B /\ B < C /\ ( ( ( F ` A ) < ( F ` B ) /\ ( F ` C ) < ( F ` B ) ) \/ ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` C ) ) ) ) ) )
34 14 25 33 rspc3ev 
 |-  ( ( ( A e. S /\ B e. S /\ C e. S ) /\ ( A < B /\ B < C /\ ( ( ( F ` A ) < ( F ` B ) /\ ( F ` C ) < ( F ` B ) ) \/ ( ( F ` B ) < ( F ` A ) /\ ( F ` B ) < ( F ` C ) ) ) ) ) -> E. a e. S E. b e. S E. c e. S ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) )
35 1 2 3 4 5 6 34 syl33anc 
 |-  ( ph -> E. a e. S E. b e. S E. c e. S ( a < b /\ b < c /\ ( ( ( F ` a ) < ( F ` b ) /\ ( F ` c ) < ( F ` b ) ) \/ ( ( F ` b ) < ( F ` a ) /\ ( F ` b ) < ( F ` c ) ) ) ) )