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 ) ) )