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 BOBasisWCOBasisWCBC=B

Proof

Step Hyp Ref Expression
1 simp3 BOBasisWCOBasisWCBCB
2 eqid 0W=0W
3 2 obsne0 BOBasisWxBx0W
4 3 3ad2antl1 BOBasisWCOBasisWCBxBx0W
5 eqid ocvW=ocvW
6 5 obselocv BOBasisWCBxBxocvWC¬xC
7 6 3expa BOBasisWCBxBxocvWC¬xC
8 7 3adantl2 BOBasisWCOBasisWCBxBxocvWC¬xC
9 simpl2 BOBasisWCOBasisWCBxBCOBasisW
10 2 5 obsocv COBasisWocvWC=0W
11 9 10 syl BOBasisWCOBasisWCBxBocvWC=0W
12 11 eleq2d BOBasisWCOBasisWCBxBxocvWCx0W
13 elsni x0Wx=0W
14 12 13 syl6bi BOBasisWCOBasisWCBxBxocvWCx=0W
15 8 14 sylbird BOBasisWCOBasisWCBxB¬xCx=0W
16 15 necon1ad BOBasisWCOBasisWCBxBx0WxC
17 4 16 mpd BOBasisWCOBasisWCBxBxC
18 1 17 eqelssd BOBasisWCOBasisWCBC=B