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 ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B → C = B

Proof

Step Hyp Ref Expression
1 simp3 ⊢ B ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B → C ⊆ B
2 eqid ⊢ 0 W = 0 W
3 2 obsne0 ⊢ B ∈ OBasis ⁡ W ∧ x ∈ B → x ≠ 0 W
4 3 3ad2antl1 ⊢ B ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B ∧ x ∈ B → x ≠ 0 W
5 eqid ⊢ ocv ⁡ W = ocv ⁡ W
6 5 obselocv ⊢ B ∈ OBasis ⁡ W ∧ C ⊆ B ∧ x ∈ B → x ∈ ocv ⁡ W ⁡ C ↔ ¬ x ∈ C
7 6 3expa ⊢ B ∈ OBasis ⁡ W ∧ C ⊆ B ∧ x ∈ B → x ∈ ocv ⁡ W ⁡ C ↔ ¬ x ∈ C
8 7 3adantl2 ⊢ B ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B ∧ x ∈ B → x ∈ ocv ⁡ W ⁡ C ↔ ¬ x ∈ C
9 simpl2 ⊢ B ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B ∧ x ∈ B → C ∈ OBasis ⁡ W
10 2 5 obsocv ⊢ C ∈ OBasis ⁡ W → ocv ⁡ W ⁡ C = 0 W
11 9 10 syl ⊢ B ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B ∧ x ∈ B → ocv ⁡ W ⁡ C = 0 W
12 11 eleq2d ⊢ B ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B ∧ x ∈ B → x ∈ ocv ⁡ W ⁡ C ↔ x ∈ 0 W
13 elsni ⊢ x ∈ 0 W → x = 0 W
14 12 13 biimtrdi ⊢ B ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B ∧ x ∈ B → x ∈ ocv ⁡ W ⁡ C → x = 0 W
15 8 14 sylbird ⊢ B ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B ∧ x ∈ B → ¬ x ∈ C → x = 0 W
16 15 necon1ad ⊢ B ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B ∧ x ∈ B → x ≠ 0 W → x ∈ C
17 4 16 mpd ⊢ B ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B ∧ x ∈ B → x ∈ C
18 1 17 eqelssd ⊢ B ∈ OBasis ⁡ W ∧ C ∈ OBasis ⁡ W ∧ C ⊆ B → C = B