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	|- A e. CH
Assertion	stge1i	|- ( S e. States -> ( 1 <_ ( S ` A ) <-> ( S ` A ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		sto1.1	|- A e. CH
2		stle1	|- ( S e. States -> ( A e. CH -> ( S ` A ) <_ 1 ) )
3	1 2	mpi	|- ( S e. States -> ( S ` A ) <_ 1 )
4	3	anim1i	|- ( ( S e. States /\ 1 <_ ( S ` A ) ) -> ( ( S ` A ) <_ 1 /\ 1 <_ ( S ` A ) ) )
5	4	ex	|- ( S e. States -> ( 1 <_ ( S ` A ) -> ( ( S ` A ) <_ 1 /\ 1 <_ ( S ` A ) ) ) )
6		stcl	|- ( S e. States -> ( A e. CH -> ( S ` A ) e. RR ) )
7	1 6	mpi	|- ( S e. States -> ( S ` A ) e. RR )
8		1re	|- 1 e. RR
9		letri3	|- ( ( ( S ` A ) e. RR /\ 1 e. RR ) -> ( ( S ` A ) = 1 <-> ( ( S ` A ) <_ 1 /\ 1 <_ ( S ` A ) ) ) )
10	7 8 9	sylancl	|- ( S e. States -> ( ( S ` A ) = 1 <-> ( ( S ` A ) <_ 1 /\ 1 <_ ( S ` A ) ) ) )
11	5 10	sylibrd	|- ( S e. States -> ( 1 <_ ( S ` A ) -> ( S ` A ) = 1 ) )
12		1le1	|- 1 <_ 1
13		breq2	|- ( ( S ` A ) = 1 -> ( 1 <_ ( S ` A ) <-> 1 <_ 1 ) )
14	12 13	mpbiri	|- ( ( S ` A ) = 1 -> 1 <_ ( S ` A ) )
15	11 14	impbid1	|- ( S e. States -> ( 1 <_ ( S ` A ) <-> ( S ` A ) = 1 ) )