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 ‘ ∅ )