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 ⊢ 𝐴 ∈ Cℋ
stle.2 ⊢ 𝐵 ∈ Cℋ
Assertion stlei ( 𝑆 ∈ States → ( 𝐴 ⊆ 𝐵 → ( 𝑆 ‘ 𝐴 ) ≤ ( 𝑆 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 stle.1 ⊢ 𝐴 ∈ Cℋ
2 stle.2 ⊢ 𝐵 ∈ Cℋ
3 2 chshii ⊢ 𝐵 ∈ Sℋ
4 shococss ⊢ ( 𝐵 ∈ Sℋ → 𝐵 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )
5 3 4 ax-mp ⊢ 𝐵 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) )
6 sstr2 ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )
7 5 6 mpi ⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) )
8 2 choccli ⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ
9 1 8 pm3.2i ⊢ ( 𝐴 ∈ Cℋ ∧ ( ⊥ ‘ 𝐵 ) ∈ Cℋ )
10 7 9 jctil ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝐴 ∈ Cℋ ∧ ( ⊥ ‘ 𝐵 ) ∈ Cℋ ) ∧ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) )
11 stj ⊢ ( 𝑆 ∈ States → ( ( ( 𝐴 ∈ Cℋ ∧ ( ⊥ ‘ 𝐵 ) ∈ Cℋ ) ∧ 𝐴 ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
12 10 11 syl5 ⊢ ( 𝑆 ∈ States → ( 𝐴 ⊆ 𝐵 → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
13 12 imp ⊢ ( ( 𝑆 ∈ States ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) )
14 1 8 chjcli ⊢ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ
15 stle1 ⊢ ( 𝑆 ∈ States → ( ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ≤ 1 ) )
16 14 15 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ≤ 1 )
17 2 sto1i ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) = 1 )
18 16 17 breqtrrd ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ≤ ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) )
19 18 adantr ⊢ ( ( 𝑆 ∈ States ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑆 ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ≤ ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) )
20 13 19 eqbrtrrd ⊢ ( ( 𝑆 ∈ States ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) ≤ ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) )
21 stcl ⊢ ( 𝑆 ∈ States → ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) ∈ ℝ ) )
22 1 21 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ∈ ℝ )
23 stcl ⊢ ( 𝑆 ∈ States → ( 𝐵 ∈ Cℋ → ( 𝑆 ‘ 𝐵 ) ∈ ℝ ) )
24 2 23 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐵 ) ∈ ℝ )
25 stcl ⊢ ( 𝑆 ∈ States → ( ( ⊥ ‘ 𝐵 ) ∈ Cℋ → ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ∈ ℝ ) )
26 8 25 mpi ⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ∈ ℝ )
27 22 24 26 3jca ⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑆 ‘ 𝐵 ) ∈ ℝ ∧ ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ∈ ℝ ) )
28 27 adantr ⊢ ( ( 𝑆 ∈ States ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑆 ‘ 𝐵 ) ∈ ℝ ∧ ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ∈ ℝ ) )
29 leadd1 ⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝑆 ‘ 𝐵 ) ∈ ℝ ∧ ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ∈ ℝ ) → ( ( 𝑆 ‘ 𝐴 ) ≤ ( 𝑆 ‘ 𝐵 ) ↔ ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) ≤ ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
30 28 29 syl ⊢ ( ( 𝑆 ∈ States ∧ 𝐴 ⊆ 𝐵 ) → ( ( 𝑆 ‘ 𝐴 ) ≤ ( 𝑆 ‘ 𝐵 ) ↔ ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) ≤ ( ( 𝑆 ‘ 𝐵 ) + ( 𝑆 ‘ ( ⊥ ‘ 𝐵 ) ) ) ) )
31 20 30 mpbird ⊢ ( ( 𝑆 ∈ States ∧ 𝐴 ⊆ 𝐵 ) → ( 𝑆 ‘ 𝐴 ) ≤ ( 𝑆 ‘ 𝐵 ) )
32 31 ex ⊢ ( 𝑆 ∈ States → ( 𝐴 ⊆ 𝐵 → ( 𝑆 ‘ 𝐴 ) ≤ ( 𝑆 ‘ 𝐵 ) ) )