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 
 |-  (/) e. _V
2 base0 
 |-  (/) = ( Base ` (/) )
3 00lss 
 |-  (/) = ( LSubSp ` (/) )
4 eqid 
 |-  ( LSpan ` (/) ) = ( LSpan ` (/) )
5 2 3 4 lspfval 
 |-  ( (/) e. _V -> ( LSpan ` (/) ) = ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } ) )
6 1 5 ax-mp 
 |-  ( LSpan ` (/) ) = ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } )
7 eqid 
 |-  ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } ) = ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } )
8 7 dmmpt 
 |-  dom ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } ) = { a e. ~P (/) | |^| { b e. (/) | a C_ b } e. _V }
9 rab0 
 |-  { b e. (/) | a C_ b } = (/)
10 9 inteqi 
 |-  |^| { b e. (/) | a C_ b } = |^| (/)
11 int0 
 |-  |^| (/) = _V
12 10 11 eqtri 
 |-  |^| { b e. (/) | a C_ b } = _V
13 vprc 
 |-  -. _V e. _V
14 12 13 eqneltri 
 |-  -. |^| { b e. (/) | a C_ b } e. _V
15 14 rgenw 
 |-  A. a e. ~P (/) -. |^| { b e. (/) | a C_ b } e. _V
16 rabeq0 
 |-  ( { a e. ~P (/) | |^| { b e. (/) | a C_ b } e. _V } = (/) <-> A. a e. ~P (/) -. |^| { b e. (/) | a C_ b } e. _V )
17 15 16 mpbir 
 |-  { a e. ~P (/) | |^| { b e. (/) | a C_ b } e. _V } = (/)
18 8 17 eqtri 
 |-  dom ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } ) = (/)
19 mptrel 
 |-  Rel ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } )
20 reldm0 
 |-  ( Rel ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } ) -> ( ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } ) = (/) <-> dom ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } ) = (/) ) )
21 19 20 ax-mp 
 |-  ( ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } ) = (/) <-> dom ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } ) = (/) )
22 18 21 mpbir 
 |-  ( a e. ~P (/) |-> |^| { b e. (/) | a C_ b } ) = (/)
23 6 22 eqtr2i 
 |-  (/) = ( LSpan ` (/) )