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