Metamath Proof Explorer


Theorem stlesi

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 stlesi ( 𝑆 ∈ States → ( 𝐴𝐵 → ( ( 𝑆𝐴 ) = 1 → ( 𝑆𝐵 ) = 1 ) ) )

Proof

Step Hyp Ref Expression
1 stle.1 𝐴C
2 stle.2 𝐵C
3 stle1 ( 𝑆 ∈ States → ( 𝐵C → ( 𝑆𝐵 ) ≤ 1 ) )
4 2 3 mpi ( 𝑆 ∈ States → ( 𝑆𝐵 ) ≤ 1 )
5 4 adantr ( ( 𝑆 ∈ States ∧ ( 𝐴𝐵 ∧ ( 𝑆𝐴 ) = 1 ) ) → ( 𝑆𝐵 ) ≤ 1 )
6 1 2 stlei ( 𝑆 ∈ States → ( 𝐴𝐵 → ( 𝑆𝐴 ) ≤ ( 𝑆𝐵 ) ) )
7 6 imp ( ( 𝑆 ∈ States ∧ 𝐴𝐵 ) → ( 𝑆𝐴 ) ≤ ( 𝑆𝐵 ) )
8 7 adantrr ( ( 𝑆 ∈ States ∧ ( 𝐴𝐵 ∧ ( 𝑆𝐴 ) = 1 ) ) → ( 𝑆𝐴 ) ≤ ( 𝑆𝐵 ) )
9 breq1 ( ( 𝑆𝐴 ) = 1 → ( ( 𝑆𝐴 ) ≤ ( 𝑆𝐵 ) ↔ 1 ≤ ( 𝑆𝐵 ) ) )
10 9 ad2antll ( ( 𝑆 ∈ States ∧ ( 𝐴𝐵 ∧ ( 𝑆𝐴 ) = 1 ) ) → ( ( 𝑆𝐴 ) ≤ ( 𝑆𝐵 ) ↔ 1 ≤ ( 𝑆𝐵 ) ) )
11 8 10 mpbid ( ( 𝑆 ∈ States ∧ ( 𝐴𝐵 ∧ ( 𝑆𝐴 ) = 1 ) ) → 1 ≤ ( 𝑆𝐵 ) )
12 stcl ( 𝑆 ∈ States → ( 𝐵C → ( 𝑆𝐵 ) ∈ ℝ ) )
13 2 12 mpi ( 𝑆 ∈ States → ( 𝑆𝐵 ) ∈ ℝ )
14 1re 1 ∈ ℝ
15 13 14 jctir ( 𝑆 ∈ States → ( ( 𝑆𝐵 ) ∈ ℝ ∧ 1 ∈ ℝ ) )
16 15 adantr ( ( 𝑆 ∈ States ∧ ( 𝐴𝐵 ∧ ( 𝑆𝐴 ) = 1 ) ) → ( ( 𝑆𝐵 ) ∈ ℝ ∧ 1 ∈ ℝ ) )
17 letri3 ( ( ( 𝑆𝐵 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑆𝐵 ) = 1 ↔ ( ( 𝑆𝐵 ) ≤ 1 ∧ 1 ≤ ( 𝑆𝐵 ) ) ) )
18 16 17 syl ( ( 𝑆 ∈ States ∧ ( 𝐴𝐵 ∧ ( 𝑆𝐴 ) = 1 ) ) → ( ( 𝑆𝐵 ) = 1 ↔ ( ( 𝑆𝐵 ) ≤ 1 ∧ 1 ≤ ( 𝑆𝐵 ) ) ) )
19 5 11 18 mpbir2and ( ( 𝑆 ∈ States ∧ ( 𝐴𝐵 ∧ ( 𝑆𝐴 ) = 1 ) ) → ( 𝑆𝐵 ) = 1 )
20 19 exp32 ( 𝑆 ∈ States → ( 𝐴𝐵 → ( ( 𝑆𝐴 ) = 1 → ( 𝑆𝐵 ) = 1 ) ) )