Step | Hyp | Ref
| Expression |
1 | | 0ex 5298 |
. . 3
β’ β
β V |
2 | | base0 17154 |
. . . 4
β’ β
=
(Baseββ
) |
3 | | 00lss 20784 |
. . . 4
β’ β
=
(LSubSpββ
) |
4 | | eqid 2724 |
. . . 4
β’
(LSpanββ
) = (LSpanββ
) |
5 | 2, 3, 4 | lspfval 20816 |
. . 3
β’ (β
β V β (LSpanββ
) = (π β π« β
β¦ β© {π
β β
β£ π
β π})) |
6 | 1, 5 | ax-mp 5 |
. 2
β’
(LSpanββ
) = (π β π« β
β¦ β© {π
β β
β£ π
β π}) |
7 | | eqid 2724 |
. . . . 5
β’ (π β π« β
β¦ β© {π β β
β£ π β π}) = (π β π« β
β¦ β© {π
β β
β£ π
β π}) |
8 | 7 | dmmpt 6230 |
. . . 4
β’ dom
(π β π« β
β¦ β© {π β β
β£ π β π}) = {π β π« β
β£ β© {π
β β
β£ π
β π} β
V} |
9 | | rab0 4375 |
. . . . . . . . 9
β’ {π β β
β£ π β π} = β
|
10 | 9 | inteqi 4945 |
. . . . . . . 8
β’ β© {π
β β
β£ π
β π} = β© β
|
11 | | int0 4957 |
. . . . . . . 8
β’ β© β
= V |
12 | 10, 11 | eqtri 2752 |
. . . . . . 7
β’ β© {π
β β
β£ π
β π} =
V |
13 | | vprc 5306 |
. . . . . . 7
β’ Β¬ V
β V |
14 | 12, 13 | eqneltri 2844 |
. . . . . 6
β’ Β¬
β© {π β β
β£ π β π} β V |
15 | 14 | rgenw 3057 |
. . . . 5
β’
βπ β
π« β
Β¬ β© {π β β
β£ π β π} β V |
16 | | rabeq0 4377 |
. . . . 5
β’ ({π β π« β
β£ β© {π β β
β£ π β π} β V} = β
β βπ β π« β
Β¬
β© {π β β
β£ π β π} β V) |
17 | 15, 16 | mpbir 230 |
. . . 4
β’ {π β π« β
β£ β© {π β β
β£ π β π} β V} = β
|
18 | 8, 17 | eqtri 2752 |
. . 3
β’ dom
(π β π« β
β¦ β© {π β β
β£ π β π}) = β
|
19 | | mptrel 5816 |
. . . 4
β’ Rel
(π β π« β
β¦ β© {π β β
β£ π β π}) |
20 | | reldm0 5918 |
. . . 4
β’ (Rel
(π β π« β
β¦ β© {π β β
β£ π β π}) β ((π β π« β
β¦ β© {π
β β
β£ π
β π}) = β
β dom (π β
π« β
β¦ β© {π β β
β£ π β π}) = β
)) |
21 | 19, 20 | ax-mp 5 |
. . 3
β’ ((π β π« β
β¦ β© {π β β
β£ π β π}) = β
β dom (π β π« β
β¦ β© {π
β β
β£ π
β π}) =
β
) |
22 | 18, 21 | mpbir 230 |
. 2
β’ (π β π« β
β¦ β© {π β β
β£ π β π}) = β
|
23 | 6, 22 | eqtr2i 2753 |
1
β’ β
=
(LSpanββ
) |