Metamath Proof Explorer

Theorem 00lsp

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

Ref Expression
Assertion 00lsp ${⊢}\varnothing =\mathrm{LSpan}\left(\varnothing \right)$

Proof

Step Hyp Ref Expression
1 0ex ${⊢}\varnothing \in \mathrm{V}$
2 base0 ${⊢}\varnothing ={\mathrm{Base}}_{\varnothing }$
3 00lss ${⊢}\varnothing =\mathrm{LSubSp}\left(\varnothing \right)$
4 eqid ${⊢}\mathrm{LSpan}\left(\varnothing \right)=\mathrm{LSpan}\left(\varnothing \right)$
5 2 3 4 lspfval ${⊢}\varnothing \in \mathrm{V}\to \mathrm{LSpan}\left(\varnothing \right)=\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)$
6 1 5 ax-mp ${⊢}\mathrm{LSpan}\left(\varnothing \right)=\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)$
7 eqid ${⊢}\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)=\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)$
8 7 dmmpt ${⊢}\mathrm{dom}\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)=\left\{{a}\in 𝒫\varnothing |\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\in \mathrm{V}\right\}$
9 rab0 ${⊢}\left\{{b}\in \varnothing |{a}\subseteq {b}\right\}=\varnothing$
10 9 inteqi ${⊢}\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}=\bigcap \varnothing$
11 int0 ${⊢}\bigcap \varnothing =\mathrm{V}$
12 10 11 eqtri ${⊢}\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}=\mathrm{V}$
13 vprc ${⊢}¬\mathrm{V}\in \mathrm{V}$
14 12 13 eqneltri ${⊢}¬\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\in \mathrm{V}$
15 14 rgenw ${⊢}\forall {a}\in 𝒫\varnothing \phantom{\rule{.4em}{0ex}}¬\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\in \mathrm{V}$
16 rabeq0 ${⊢}\left\{{a}\in 𝒫\varnothing |\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\in \mathrm{V}\right\}=\varnothing ↔\forall {a}\in 𝒫\varnothing \phantom{\rule{.4em}{0ex}}¬\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\in \mathrm{V}$
17 15 16 mpbir ${⊢}\left\{{a}\in 𝒫\varnothing |\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\in \mathrm{V}\right\}=\varnothing$
18 8 17 eqtri ${⊢}\mathrm{dom}\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)=\varnothing$
19 mptrel ${⊢}\mathrm{Rel}\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)$
20 reldm0 ${⊢}\mathrm{Rel}\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)\to \left(\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)=\varnothing ↔\mathrm{dom}\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)=\varnothing \right)$
21 19 20 ax-mp ${⊢}\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)=\varnothing ↔\mathrm{dom}\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)=\varnothing$
22 18 21 mpbir ${⊢}\left({a}\in 𝒫\varnothing ⟼\bigcap \left\{{b}\in \varnothing |{a}\subseteq {b}\right\}\right)=\varnothing$
23 6 22 eqtr2i ${⊢}\varnothing =\mathrm{LSpan}\left(\varnothing \right)$