| Step | Hyp | Ref
| Expression |
|---|
| 1 | | elex 3492 |
. . . . 5
β’ (π β π β π β V) |
| 2 | | fveq2 6902 |
. . . . . . . 8
β’ (π€ = π β (Baseβπ€) = (Baseβπ)) |
| 3 | 2 | pweqd 4623 |
. . . . . . 7
β’ (π€ = π β π« (Baseβπ€) = π« (Baseβπ)) |
| 4 | | breq2 5156 |
. . . . . . 7
β’ (π€ = π β (( I βΎ π ) LIndF π€ β ( I βΎ π ) LIndF π)) |
| 5 | 3, 4 | rabeqbidv 3448 |
. . . . . 6
β’ (π€ = π β {π β π« (Baseβπ€) β£ ( I βΎ π ) LIndF π€} = {π β π« (Baseβπ) β£ ( I βΎ π ) LIndF π}) |
| 6 | | df-linds 21748 |
. . . . . 6
β’ LIndS =
(π€ β V β¦ {π β π«
(Baseβπ€) β£ ( I
βΎ π ) LIndF π€}) |
| 7 | | fvex 6915 |
. . . . . . . 8
β’
(Baseβπ)
β V |
| 8 | 7 | pwex 5384 |
. . . . . . 7
β’ π«
(Baseβπ) β
V |
| 9 | 8 | rabex 5338 |
. . . . . 6
β’ {π β π«
(Baseβπ) β£ ( I
βΎ π ) LIndF π} β V |
| 10 | 5, 6, 9 | fvmpt 7010 |
. . . . 5
β’ (π β V β
(LIndSβπ) = {π β π«
(Baseβπ) β£ ( I
βΎ π ) LIndF π}) |
| 11 | 1, 10 | syl 17 |
. . . 4
β’ (π β π β (LIndSβπ) = {π β π« (Baseβπ) β£ ( I βΎ π ) LIndF π}) |
| 12 | 11 | eleq2d 2815 |
. . 3
β’ (π β π β (π β (LIndSβπ) β π β {π β π« (Baseβπ) β£ ( I βΎ π ) LIndF π})) |
| 13 | | reseq2 5984 |
. . . . 5
β’ (π = π β ( I βΎ π ) = ( I βΎ π)) |
| 14 | 13 | breq1d 5162 |
. . . 4
β’ (π = π β (( I βΎ π ) LIndF π β ( I βΎ π) LIndF π)) |
| 15 | 14 | elrab 3684 |
. . 3
β’ (π β {π β π« (Baseβπ) β£ ( I βΎ π ) LIndF π} β (π β π« (Baseβπ) β§ ( I βΎ π) LIndF π)) |
| 16 | 12, 15 | bitrdi 286 |
. 2
β’ (π β π β (π β (LIndSβπ) β (π β π« (Baseβπ) β§ ( I βΎ π) LIndF π))) |
| 17 | 7 | elpw2 5351 |
. . . 4
β’ (π β π«
(Baseβπ) β π β (Baseβπ)) |
| 18 | | islinds.b |
. . . . 5
β’ π΅ = (Baseβπ) |
| 19 | 18 | sseq2i 4011 |
. . . 4
β’ (π β π΅ β π β (Baseβπ)) |
| 20 | 17, 19 | bitr4i 277 |
. . 3
β’ (π β π«
(Baseβπ) β π β π΅) |
| 21 | 20 | anbi1i 622 |
. 2
β’ ((π β π«
(Baseβπ) β§ ( I
βΎ π) LIndF π) β (π β π΅ β§ ( I βΎ π) LIndF π)) |
| 22 | 16, 21 | bitrdi 286 |
1
β’ (π β π β (π β (LIndSβπ) β (π β π΅ β§ ( I βΎ π) LIndF π))) |
