Metamath Proof Explorer

Theorem 00lsp

Description: fvco4i lemma for linear spans. (Contributed by Stefan O'Rear, 4-Apr-2015)

Ref Expression
Assertion 00lsp ⊢ ∅ = LSpan ⁡ ∅

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 base0 ⊢ ∅ = Base ∅
3 00lss ⊢ ∅ = LSubSp ⁡ ∅
4 eqid ⊢ LSpan ⁡ ∅ = LSpan ⁡ ∅
5 2 3 4 lspfval ⊢ ∅ ∈ V → LSpan ⁡ ∅ = a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b
6 1 5 ax-mp ⊢ LSpan ⁡ ∅ = a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b
7 eqid ⊢ a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b = a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b
8 7 dmmpt ⊢ dom ⁡ a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b = a ∈ 𝒫 ∅ | ⋂ b ∈ ∅ | a ⊆ b ∈ V
9 rab0 ⊢ b ∈ ∅ | a ⊆ b = ∅
10 9 inteqi ⊢ ⋂ b ∈ ∅ | a ⊆ b = ⋂ ∅
11 int0 ⊢ ⋂ ∅ = V
12 10 11 eqtri ⊢ ⋂ b ∈ ∅ | a ⊆ b = V
13 vprc ⊢ ¬ V ∈ V
14 12 13 eqneltri ⊢ ¬ ⋂ b ∈ ∅ | a ⊆ b ∈ V
15 14 rgenw ⊢ ∀ a ∈ 𝒫 ∅ ¬ ⋂ b ∈ ∅ | a ⊆ b ∈ V
16 rabeq0 ⊢ a ∈ 𝒫 ∅ | ⋂ b ∈ ∅ | a ⊆ b ∈ V = ∅ ↔ ∀ a ∈ 𝒫 ∅ ¬ ⋂ b ∈ ∅ | a ⊆ b ∈ V
17 15 16 mpbir ⊢ a ∈ 𝒫 ∅ | ⋂ b ∈ ∅ | a ⊆ b ∈ V = ∅
18 8 17 eqtri ⊢ dom ⁡ a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b = ∅
19 mptrel ⊢ Rel ⁡ a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b
20 reldm0 ⊢ Rel ⁡ a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b → a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b = ∅ ↔ dom ⁡ a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b = ∅
21 19 20 ax-mp ⊢ a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b = ∅ ↔ dom ⁡ a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b = ∅
22 18 21 mpbir ⊢ a ∈ 𝒫 ∅ ⟼ ⋂ b ∈ ∅ | a ⊆ b = ∅
23 6 22 eqtr2i ⊢ ∅ = LSpan ⁡ ∅