Theorem lssuni

Description: The union of all subspaces is the vector space. (Contributed by NM, 13-Mar-2015)

	Ref	Expression
Hypotheses	lssss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lssss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
	lssuni.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
Assertion	lssuni	⊢ ( 𝜑 → ∪ 𝑆 = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		lssss.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lssss.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		lssuni.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
4		rabid2	⊢ ( 𝑆 = { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑉 } ↔ ∀ 𝑥 ∈ 𝑆 𝑥 ⊆ 𝑉 )
5	1 2	lssss	⊢ ( 𝑥 ∈ 𝑆 → 𝑥 ⊆ 𝑉 )
6	4 5	mprgbir	⊢ 𝑆 = { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑉 }
7	6	unieqi	⊢ ∪ 𝑆 = ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑉 }
8	1 2	lss1	⊢ ( 𝑊 ∈ LMod → 𝑉 ∈ 𝑆 )
9		unimax	⊢ ( 𝑉 ∈ 𝑆 → ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑉 } = 𝑉 )
10	3 8 9	3syl	⊢ ( 𝜑 → ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑉 } = 𝑉 )
11	7 10	eqtrid	⊢ ( 𝜑 → ∪ 𝑆 = 𝑉 )