Step | Hyp | Ref
| Expression |
1 | | elex 3462 |
. . . . 5
β’ (π β π β π β V) |
2 | | fveq2 6843 |
. . . . . . . 8
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
3 | 2 | pweqd 4578 |
. . . . . . 7
β’ (π€ = π β π« (Baseβπ€) = π« (Baseβπ)) |
4 | | breq2 5110 |
. . . . . . 7
β’ (π€ = π β (( I βΎ π ) LIndF π€ β ( I βΎ π ) LIndF π)) |
5 | 3, 4 | rabeqbidv 3423 |
. . . . . 6
β’ (π€ = π β {π β π« (Baseβπ€) β£ ( I βΎ π ) LIndF π€} = {π β π« (Baseβπ) β£ ( I βΎ π ) LIndF π}) |
6 | | df-linds 21229 |
. . . . . 6
β’ LIndS =
(π€ β V β¦ {π β π«
(Baseβπ€) β£ ( I
βΎ π ) LIndF π€}) |
7 | | fvex 6856 |
. . . . . . . 8
β’
(Baseβπ)
β V |
8 | 7 | pwex 5336 |
. . . . . . 7
β’ π«
(Baseβπ) β
V |
9 | 8 | rabex 5290 |
. . . . . 6
β’ {π β π«
(Baseβπ) β£ ( I
βΎ π ) LIndF π} β V |
10 | 5, 6, 9 | fvmpt 6949 |
. . . . 5
β’ (π β V β
(LIndSβπ) = {π β π«
(Baseβπ) β£ ( I
βΎ π ) LIndF π}) |
11 | 1, 10 | syl 17 |
. . . 4
β’ (π β π β (LIndSβπ) = {π β π« (Baseβπ) β£ ( I βΎ π ) LIndF π}) |
12 | 11 | eleq2d 2820 |
. . 3
β’ (π β π β (π β (LIndSβπ) β π β {π β π« (Baseβπ) β£ ( I βΎ π ) LIndF π})) |
13 | | reseq2 5933 |
. . . . 5
β’ (π = π β ( I βΎ π ) = ( I βΎ π)) |
14 | 13 | breq1d 5116 |
. . . 4
β’ (π = π β (( I βΎ π ) LIndF π β ( I βΎ π) LIndF π)) |
15 | 14 | elrab 3646 |
. . 3
β’ (π β {π β π« (Baseβπ) β£ ( I βΎ π ) LIndF π} β (π β π« (Baseβπ) β§ ( I βΎ π) LIndF π)) |
16 | 12, 15 | bitrdi 287 |
. 2
β’ (π β π β (π β (LIndSβπ) β (π β π« (Baseβπ) β§ ( I βΎ π) LIndF π))) |
17 | 7 | elpw2 5303 |
. . . 4
β’ (π β π«
(Baseβπ) β π β (Baseβπ)) |
18 | | islinds.b |
. . . . 5
β’ π΅ = (Baseβπ) |
19 | 18 | sseq2i 3974 |
. . . 4
β’ (π β π΅ β π β (Baseβπ)) |
20 | 17, 19 | bitr4i 278 |
. . 3
β’ (π β π«
(Baseβπ) β π β π΅) |
21 | 20 | anbi1i 625 |
. 2
β’ ((π β π«
(Baseβπ) β§ ( I
βΎ π) LIndF π) β (π β π΅ β§ ( I βΎ π) LIndF π)) |
22 | 16, 21 | bitrdi 287 |
1
β’ (π β π β (π β (LIndSβπ) β (π β π΅ β§ ( I βΎ π) LIndF π))) |