Metamath Proof Explorer

Theorem obs2ss

Description: A basis has no proper subsets that are also bases. (Contributed by Mario Carneiro, 23-Oct-2015)

Ref Expression
Assertion obs2ss 
|- ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) -> C = B )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) -> C C_ B )
2 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
3 2 obsne0 
 |-  ( ( B e. ( OBasis ` W ) /\ x e. B ) -> x =/= ( 0g ` W ) )
4 3 3ad2antl1 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) /\ x e. B ) -> x =/= ( 0g ` W ) )
5 eqid 
 |-  ( ocv ` W ) = ( ocv ` W )
6 5 obselocv 
 |-  ( ( B e. ( OBasis ` W ) /\ C C_ B /\ x e. B ) -> ( x e. ( ( ocv ` W ) ` C ) <-> -. x e. C ) )
7 6 3expa 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C C_ B ) /\ x e. B ) -> ( x e. ( ( ocv ` W ) ` C ) <-> -. x e. C ) )
8 7 3adantl2 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) /\ x e. B ) -> ( x e. ( ( ocv ` W ) ` C ) <-> -. x e. C ) )
9 simpl2 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) /\ x e. B ) -> C e. ( OBasis ` W ) )
10 2 5 obsocv 
 |-  ( C e. ( OBasis ` W ) -> ( ( ocv ` W ) ` C ) = { ( 0g ` W ) } )
11 9 10 syl 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) /\ x e. B ) -> ( ( ocv ` W ) ` C ) = { ( 0g ` W ) } )
12 11 eleq2d 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) /\ x e. B ) -> ( x e. ( ( ocv ` W ) ` C ) <-> x e. { ( 0g ` W ) } ) )
13 elsni 
 |-  ( x e. { ( 0g ` W ) } -> x = ( 0g ` W ) )
14 12 13 biimtrdi 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) /\ x e. B ) -> ( x e. ( ( ocv ` W ) ` C ) -> x = ( 0g ` W ) ) )
15 8 14 sylbird 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) /\ x e. B ) -> ( -. x e. C -> x = ( 0g ` W ) ) )
16 15 necon1ad 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) /\ x e. B ) -> ( x =/= ( 0g ` W ) -> x e. C ) )
17 4 16 mpd 
 |-  ( ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) /\ x e. B ) -> x e. C )
18 1 17 eqelssd 
 |-  ( ( B e. ( OBasis ` W ) /\ C e. ( OBasis ` W ) /\ C C_ B ) -> C = B )