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