This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ ∅ ) = ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ) )
6 1 5 ax-mp ⊢ ( LSpan ‘ ∅ ) = ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } )
7 eqid ⊢ ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ) = ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } )
8 7 dmmpt ⊢ dom ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ) = { 𝑎 ∈ 𝒫 ∅ ∣ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ∈ V }
9 rab0 ⊢ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } = ∅
10 9 inteqi ⊢ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } = ∩ ∅
11 int0 ⊢ ∩ ∅ = V
12 10 11 eqtri ⊢ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } = V
13 vprc ⊢ ¬ V ∈ V
14 12 13 eqneltri ⊢ ¬ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ∈ V
15 14 rgenw ⊢ ∀ 𝑎 ∈ 𝒫 ∅ ¬ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ∈ V
16 rabeq0 ⊢ ( { 𝑎 ∈ 𝒫 ∅ ∣ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ∈ V } = ∅ ↔ ∀ 𝑎 ∈ 𝒫 ∅ ¬ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ∈ V )
17 15 16 mpbir ⊢ { 𝑎 ∈ 𝒫 ∅ ∣ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ∈ V } = ∅
18 8 17 eqtri ⊢ dom ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ) = ∅
19 mptrel ⊢ Rel ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } )
20 reldm0 ⊢ ( Rel ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ) → ( ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ) = ∅ ↔ dom ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ) = ∅ ) )
21 19 20 ax-mp ⊢ ( ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ) = ∅ ↔ dom ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ) = ∅ )
22 18 21 mpbir ⊢ ( 𝑎 ∈ 𝒫 ∅ ↦ ∩ { 𝑏 ∈ ∅ ∣ 𝑎 ⊆ 𝑏 } ) = ∅
23 6 22 eqtr2i ⊢ ∅ = ( LSpan ‘ ∅ )