Metamath Proof Explorer

Theorem stlei

Description: Ordering law for states. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses stle.1 
|- A e. CH
stle.2 
|- B e. CH
Assertion stlei 
|- ( S e. States -> ( A C_ B -> ( S ` A ) <_ ( S ` B ) ) )

Proof

Step Hyp Ref Expression
1 stle.1 
 |-  A e. CH
2 stle.2 
 |-  B e. CH
3 2 chshii 
 |-  B e. SH
4 shococss 
 |-  ( B e. SH -> B C_ ( _|_ ` ( _|_ ` B ) ) )
5 3 4 ax-mp 
 |-  B C_ ( _|_ ` ( _|_ ` B ) )
6 sstr2 
 |-  ( A C_ B -> ( B C_ ( _|_ ` ( _|_ ` B ) ) -> A C_ ( _|_ ` ( _|_ ` B ) ) ) )
7 5 6 mpi 
 |-  ( A C_ B -> A C_ ( _|_ ` ( _|_ ` B ) ) )
8 2 choccli 
 |-  ( _|_ ` B ) e. CH
9 1 8 pm3.2i 
 |-  ( A e. CH /\ ( _|_ ` B ) e. CH )
10 7 9 jctil 
 |-  ( A C_ B -> ( ( A e. CH /\ ( _|_ ` B ) e. CH ) /\ A C_ ( _|_ ` ( _|_ ` B ) ) ) )
11 stj 
 |-  ( S e. States -> ( ( ( A e. CH /\ ( _|_ ` B ) e. CH ) /\ A C_ ( _|_ ` ( _|_ ` B ) ) ) -> ( S ` ( A vH ( _|_ ` B ) ) ) = ( ( S ` A ) + ( S ` ( _|_ ` B ) ) ) ) )
12 10 11 syl5 
 |-  ( S e. States -> ( A C_ B -> ( S ` ( A vH ( _|_ ` B ) ) ) = ( ( S ` A ) + ( S ` ( _|_ ` B ) ) ) ) )
13 12 imp 
 |-  ( ( S e. States /\ A C_ B ) -> ( S ` ( A vH ( _|_ ` B ) ) ) = ( ( S ` A ) + ( S ` ( _|_ ` B ) ) ) )
14 1 8 chjcli 
 |-  ( A vH ( _|_ ` B ) ) e. CH
15 stle1 
 |-  ( S e. States -> ( ( A vH ( _|_ ` B ) ) e. CH -> ( S ` ( A vH ( _|_ ` B ) ) ) <_ 1 ) )
16 14 15 mpi 
 |-  ( S e. States -> ( S ` ( A vH ( _|_ ` B ) ) ) <_ 1 )
17 2 sto1i 
 |-  ( S e. States -> ( ( S ` B ) + ( S ` ( _|_ ` B ) ) ) = 1 )
18 16 17 breqtrrd 
 |-  ( S e. States -> ( S ` ( A vH ( _|_ ` B ) ) ) <_ ( ( S ` B ) + ( S ` ( _|_ ` B ) ) ) )
19 18 adantr 
 |-  ( ( S e. States /\ A C_ B ) -> ( S ` ( A vH ( _|_ ` B ) ) ) <_ ( ( S ` B ) + ( S ` ( _|_ ` B ) ) ) )
20 13 19 eqbrtrrd 
 |-  ( ( S e. States /\ A C_ B ) -> ( ( S ` A ) + ( S ` ( _|_ ` B ) ) ) <_ ( ( S ` B ) + ( S ` ( _|_ ` B ) ) ) )
21 stcl 
 |-  ( S e. States -> ( A e. CH -> ( S ` A ) e. RR ) )
22 1 21 mpi 
 |-  ( S e. States -> ( S ` A ) e. RR )
23 stcl 
 |-  ( S e. States -> ( B e. CH -> ( S ` B ) e. RR ) )
24 2 23 mpi 
 |-  ( S e. States -> ( S ` B ) e. RR )
25 stcl 
 |-  ( S e. States -> ( ( _|_ ` B ) e. CH -> ( S ` ( _|_ ` B ) ) e. RR ) )
26 8 25 mpi 
 |-  ( S e. States -> ( S ` ( _|_ ` B ) ) e. RR )
27 22 24 26 3jca 
 |-  ( S e. States -> ( ( S ` A ) e. RR /\ ( S ` B ) e. RR /\ ( S ` ( _|_ ` B ) ) e. RR ) )
28 27 adantr 
 |-  ( ( S e. States /\ A C_ B ) -> ( ( S ` A ) e. RR /\ ( S ` B ) e. RR /\ ( S ` ( _|_ ` B ) ) e. RR ) )
29 leadd1 
 |-  ( ( ( S ` A ) e. RR /\ ( S ` B ) e. RR /\ ( S ` ( _|_ ` B ) ) e. RR ) -> ( ( S ` A ) <_ ( S ` B ) <-> ( ( S ` A ) + ( S ` ( _|_ ` B ) ) ) <_ ( ( S ` B ) + ( S ` ( _|_ ` B ) ) ) ) )
30 28 29 syl 
 |-  ( ( S e. States /\ A C_ B ) -> ( ( S ` A ) <_ ( S ` B ) <-> ( ( S ` A ) + ( S ` ( _|_ ` B ) ) ) <_ ( ( S ` B ) + ( S ` ( _|_ ` B ) ) ) ) )
31 20 30 mpbird 
 |-  ( ( S e. States /\ A C_ B ) -> ( S ` A ) <_ ( S ` B ) )
32 31 ex 
 |-  ( S e. States -> ( A C_ B -> ( S ` A ) <_ ( S ` B ) ) )