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⁡∅