Metamath Proof Explorer

Theorem stcltr1i

Description: Property of a strong classical state. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses stcltr1.1 
|- ( ph <-> ( S e. States /\ A. x e. CH A. y e. CH ( ( ( S ` x ) = 1 -> ( S ` y ) = 1 ) -> x C_ y ) ) )
stcltr1.2 
|- A e. CH
stcltr1.3 
|- B e. CH
Assertion stcltr1i 
|- ( ph -> ( ( ( S ` A ) = 1 -> ( S ` B ) = 1 ) -> A C_ B ) )

Proof

Step Hyp Ref Expression
1 stcltr1.1 
 |-  ( ph <-> ( S e. States /\ A. x e. CH A. y e. CH ( ( ( S ` x ) = 1 -> ( S ` y ) = 1 ) -> x C_ y ) ) )
2 stcltr1.2 
 |-  A e. CH
3 stcltr1.3 
 |-  B e. CH
4 fveqeq2 
 |-  ( x = A -> ( ( S ` x ) = 1 <-> ( S ` A ) = 1 ) )
5 4 imbi1d 
 |-  ( x = A -> ( ( ( S ` x ) = 1 -> ( S ` y ) = 1 ) <-> ( ( S ` A ) = 1 -> ( S ` y ) = 1 ) ) )
6 sseq1 
 |-  ( x = A -> ( x C_ y <-> A C_ y ) )
7 5 6 imbi12d 
 |-  ( x = A -> ( ( ( ( S ` x ) = 1 -> ( S ` y ) = 1 ) -> x C_ y ) <-> ( ( ( S ` A ) = 1 -> ( S ` y ) = 1 ) -> A C_ y ) ) )
8 fveqeq2 
 |-  ( y = B -> ( ( S ` y ) = 1 <-> ( S ` B ) = 1 ) )
9 8 imbi2d 
 |-  ( y = B -> ( ( ( S ` A ) = 1 -> ( S ` y ) = 1 ) <-> ( ( S ` A ) = 1 -> ( S ` B ) = 1 ) ) )
10 sseq2 
 |-  ( y = B -> ( A C_ y <-> A C_ B ) )
11 9 10 imbi12d 
 |-  ( y = B -> ( ( ( ( S ` A ) = 1 -> ( S ` y ) = 1 ) -> A C_ y ) <-> ( ( ( S ` A ) = 1 -> ( S ` B ) = 1 ) -> A C_ B ) ) )
12 7 11 rspc2v 
 |-  ( ( A e. CH /\ B e. CH ) -> ( A. x e. CH A. y e. CH ( ( ( S ` x ) = 1 -> ( S ` y ) = 1 ) -> x C_ y ) -> ( ( ( S ` A ) = 1 -> ( S ` B ) = 1 ) -> A C_ B ) ) )
13 2 3 12 mp2an 
 |-  ( A. x e. CH A. y e. CH ( ( ( S ` x ) = 1 -> ( S ` y ) = 1 ) -> x C_ y ) -> ( ( ( S ` A ) = 1 -> ( S ` B ) = 1 ) -> A C_ B ) )
14 1 13 simplbiim 
 |-  ( ph -> ( ( ( S ` A ) = 1 -> ( S ` B ) = 1 ) -> A C_ B ) )