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 ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) → 𝐶 = 𝐵 )

Proof

Step Hyp Ref Expression
1 simp3 ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) → 𝐶𝐵 )
2 eqid ( 0g𝑊 ) = ( 0g𝑊 )
3 2 obsne0 ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝑥𝐵 ) → 𝑥 ≠ ( 0g𝑊 ) )
4 3 3ad2antl1 ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) ∧ 𝑥𝐵 ) → 𝑥 ≠ ( 0g𝑊 ) )
5 eqid ( ocv ‘ 𝑊 ) = ( ocv ‘ 𝑊 )
6 5 obselocv ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵𝑥𝐵 ) → ( 𝑥 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝐶 ) ↔ ¬ 𝑥𝐶 ) )
7 6 3expa ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) ∧ 𝑥𝐵 ) → ( 𝑥 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝐶 ) ↔ ¬ 𝑥𝐶 ) )
8 7 3adantl2 ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) ∧ 𝑥𝐵 ) → ( 𝑥 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝐶 ) ↔ ¬ 𝑥𝐶 ) )
9 simpl2 ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) ∧ 𝑥𝐵 ) → 𝐶 ∈ ( OBasis ‘ 𝑊 ) )
10 2 5 obsocv ( 𝐶 ∈ ( OBasis ‘ 𝑊 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝐶 ) = { ( 0g𝑊 ) } )
11 9 10 syl ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) ∧ 𝑥𝐵 ) → ( ( ocv ‘ 𝑊 ) ‘ 𝐶 ) = { ( 0g𝑊 ) } )
12 11 eleq2d ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) ∧ 𝑥𝐵 ) → ( 𝑥 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝐶 ) ↔ 𝑥 ∈ { ( 0g𝑊 ) } ) )
13 elsni ( 𝑥 ∈ { ( 0g𝑊 ) } → 𝑥 = ( 0g𝑊 ) )
14 12 13 syl6bi ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) ∧ 𝑥𝐵 ) → ( 𝑥 ∈ ( ( ocv ‘ 𝑊 ) ‘ 𝐶 ) → 𝑥 = ( 0g𝑊 ) ) )
15 8 14 sylbird ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) ∧ 𝑥𝐵 ) → ( ¬ 𝑥𝐶𝑥 = ( 0g𝑊 ) ) )
16 15 necon1ad ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) ∧ 𝑥𝐵 ) → ( 𝑥 ≠ ( 0g𝑊 ) → 𝑥𝐶 ) )
17 4 16 mpd ( ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) ∧ 𝑥𝐵 ) → 𝑥𝐶 )
18 1 17 eqelssd ( ( 𝐵 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶 ∈ ( OBasis ‘ 𝑊 ) ∧ 𝐶𝐵 ) → 𝐶 = 𝐵 )