Metamath Proof Explorer

Theorem lsatlspsn

Description: The span of a nonzero singleton is an atom. (Contributed by NM, 16-Jan-2015)

Ref Expression
Hypotheses lsatset.v ⊢ V = Base W
lsatset.n ⊢ N = LSpan ⁡ W
lsatset.z ⊢ 0 ˙ = 0 W
lsatset.a ⊢ A = LSAtoms ⁡ W
lsatlspsn.w ⊢ φ → W ∈ LMod
lsatlspsn.x ⊢ φ → X ∈ V ∖ 0 ˙
Assertion lsatlspsn ⊢ φ → N ⁡ X ∈ A

Proof

Step Hyp Ref Expression
1 lsatset.v ⊢ V = Base W
2 lsatset.n ⊢ N = LSpan ⁡ W
3 lsatset.z ⊢ 0 ˙ = 0 W
4 lsatset.a ⊢ A = LSAtoms ⁡ W
5 lsatlspsn.w ⊢ φ → W ∈ LMod
6 lsatlspsn.x ⊢ φ → X ∈ V ∖ 0 ˙
7 eqid ⊢ N ⁡ X = N ⁡ X
8 sneq ⊢ v = X → v = X
9 8 fveq2d ⊢ v = X → N ⁡ v = N ⁡ X
10 9 rspceeqv ⊢ X ∈ V ∖ 0 ˙ ∧ N ⁡ X = N ⁡ X → ∃ v ∈ V ∖ 0 ˙ N ⁡ X = N ⁡ v
11 6 7 10 sylancl ⊢ φ → ∃ v ∈ V ∖ 0 ˙ N ⁡ X = N ⁡ v
12 1 2 3 4 islsat ⊢ W ∈ LMod → N ⁡ X ∈ A ↔ ∃ v ∈ V ∖ 0 ˙ N ⁡ X = N ⁡ v
13 5 12 syl ⊢ φ → N ⁡ X ∈ A ↔ ∃ v ∈ V ∖ 0 ˙ N ⁡ X = N ⁡ v
14 11 13 mpbird ⊢ φ → N ⁡ X ∈ A