Step | Hyp | Ref
| Expression |
1 | | 0ex 5265 |
. . 3
β’ β
β V |
2 | | base0 17093 |
. . . 4
β’ β
=
(Baseββ
) |
3 | | 00lss 20417 |
. . . 4
β’ β
=
(LSubSpββ
) |
4 | | eqid 2733 |
. . . 4
β’
(LSpanββ
) = (LSpanββ
) |
5 | 2, 3, 4 | lspfval 20449 |
. . 3
β’ (β
β V β (LSpanββ
) = (π β π« β
β¦ β© {π
β β
β£ π
β π})) |
6 | 1, 5 | ax-mp 5 |
. 2
β’
(LSpanββ
) = (π β π« β
β¦ β© {π
β β
β£ π
β π}) |
7 | | eqid 2733 |
. . . . 5
β’ (π β π« β
β¦ β© {π β β
β£ π β π}) = (π β π« β
β¦ β© {π
β β
β£ π
β π}) |
8 | 7 | dmmpt 6193 |
. . . 4
β’ dom
(π β π« β
β¦ β© {π β β
β£ π β π}) = {π β π« β
β£ β© {π
β β
β£ π
β π} β
V} |
9 | | rab0 4343 |
. . . . . . . . 9
β’ {π β β
β£ π β π} = β
|
10 | 9 | inteqi 4912 |
. . . . . . . 8
β’ β© {π
β β
β£ π
β π} = β© β
|
11 | | int0 4924 |
. . . . . . . 8
β’ β© β
= V |
12 | 10, 11 | eqtri 2761 |
. . . . . . 7
β’ β© {π
β β
β£ π
β π} =
V |
13 | | vprc 5273 |
. . . . . . 7
β’ Β¬ V
β V |
14 | 12, 13 | eqneltri 2853 |
. . . . . 6
β’ Β¬
β© {π β β
β£ π β π} β V |
15 | 14 | rgenw 3065 |
. . . . 5
β’
βπ β
π« β
Β¬ β© {π β β
β£ π β π} β V |
16 | | rabeq0 4345 |
. . . . 5
β’ ({π β π« β
β£ β© {π β β
β£ π β π} β V} = β
β βπ β π« β
Β¬
β© {π β β
β£ π β π} β V) |
17 | 15, 16 | mpbir 230 |
. . . 4
β’ {π β π« β
β£ β© {π β β
β£ π β π} β V} = β
|
18 | 8, 17 | eqtri 2761 |
. . 3
β’ dom
(π β π« β
β¦ β© {π β β
β£ π β π}) = β
|
19 | | mptrel 5782 |
. . . 4
β’ Rel
(π β π« β
β¦ β© {π β β
β£ π β π}) |
20 | | reldm0 5884 |
. . . 4
β’ (Rel
(π β π« β
β¦ β© {π β β
β£ π β π}) β ((π β π« β
β¦ β© {π
β β
β£ π
β π}) = β
β dom (π β
π« β
β¦ β© {π β β
β£ π β π}) = β
)) |
21 | 19, 20 | ax-mp 5 |
. . 3
β’ ((π β π« β
β¦ β© {π β β
β£ π β π}) = β
β dom (π β π« β
β¦ β© {π
β β
β£ π
β π}) =
β
) |
22 | 18, 21 | mpbir 230 |
. 2
β’ (π β π« β
β¦ β© {π β β
β£ π β π}) = β
|
23 | 6, 22 | eqtr2i 2762 |
1
β’ β
=
(LSpanββ
) |