Theorem stge1i

Description: If a state is greater than or equal to 1, it is 1. (Contributed by NM, 11-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sto1.1	⊢ 𝐴 ∈ Cℋ
Assertion	stge1i	⊢ ( 𝑆 ∈ States → ( 1 ≤ ( 𝑆 ‘ 𝐴 ) ↔ ( 𝑆 ‘ 𝐴 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		sto1.1	⊢ 𝐴 ∈ Cℋ
2		stle1	⊢ ( 𝑆 ∈ States → ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) ≤ 1 ) )
3	1 2	mpi	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ≤ 1 )
4	3	anim1i	⊢ ( ( 𝑆 ∈ States ∧ 1 ≤ ( 𝑆 ‘ 𝐴 ) ) → ( ( 𝑆 ‘ 𝐴 ) ≤ 1 ∧ 1 ≤ ( 𝑆 ‘ 𝐴 ) ) )
5	4	ex	⊢ ( 𝑆 ∈ States → ( 1 ≤ ( 𝑆 ‘ 𝐴 ) → ( ( 𝑆 ‘ 𝐴 ) ≤ 1 ∧ 1 ≤ ( 𝑆 ‘ 𝐴 ) ) ) )
6		stcl	⊢ ( 𝑆 ∈ States → ( 𝐴 ∈ Cℋ → ( 𝑆 ‘ 𝐴 ) ∈ ℝ ) )
7	1 6	mpi	⊢ ( 𝑆 ∈ States → ( 𝑆 ‘ 𝐴 ) ∈ ℝ )
8		1re	⊢ 1 ∈ ℝ
9		letri3	⊢ ( ( ( 𝑆 ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( 𝑆 ‘ 𝐴 ) = 1 ↔ ( ( 𝑆 ‘ 𝐴 ) ≤ 1 ∧ 1 ≤ ( 𝑆 ‘ 𝐴 ) ) ) )
10	7 8 9	sylancl	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ 𝐴 ) = 1 ↔ ( ( 𝑆 ‘ 𝐴 ) ≤ 1 ∧ 1 ≤ ( 𝑆 ‘ 𝐴 ) ) ) )
11	5 10	sylibrd	⊢ ( 𝑆 ∈ States → ( 1 ≤ ( 𝑆 ‘ 𝐴 ) → ( 𝑆 ‘ 𝐴 ) = 1 ) )
12		1le1	⊢ 1 ≤ 1
13		breq2	⊢ ( ( 𝑆 ‘ 𝐴 ) = 1 → ( 1 ≤ ( 𝑆 ‘ 𝐴 ) ↔ 1 ≤ 1 ) )
14	12 13	mpbiri	⊢ ( ( 𝑆 ‘ 𝐴 ) = 1 → 1 ≤ ( 𝑆 ‘ 𝐴 ) )
15	11 14	impbid1	⊢ ( 𝑆 ∈ States → ( 1 ≤ ( 𝑆 ‘ 𝐴 ) ↔ ( 𝑆 ‘ 𝐴 ) = 1 ) )