Step | Hyp | Ref
| Expression |
1 | | lbsext.c |
. . . 4
β’ (π β πΆ β π) |
2 | | lbsext.v |
. . . . . 6
β’ π = (Baseβπ) |
3 | 2 | fvexi 6860 |
. . . . 5
β’ π β V |
4 | 3 | elpw2 5306 |
. . . 4
β’ (πΆ β π« π β πΆ β π) |
5 | 1, 4 | sylibr 233 |
. . 3
β’ (π β πΆ β π« π) |
6 | | lbsext.x |
. . . 4
β’ (π β βπ₯ β πΆ Β¬ π₯ β (πβ(πΆ β {π₯}))) |
7 | | ssid 3970 |
. . . 4
β’ πΆ β πΆ |
8 | 6, 7 | jctil 521 |
. . 3
β’ (π β (πΆ β πΆ β§ βπ₯ β πΆ Β¬ π₯ β (πβ(πΆ β {π₯})))) |
9 | | sseq2 3974 |
. . . . 5
β’ (π§ = πΆ β (πΆ β π§ β πΆ β πΆ)) |
10 | | difeq1 4079 |
. . . . . . . . 9
β’ (π§ = πΆ β (π§ β {π₯}) = (πΆ β {π₯})) |
11 | 10 | fveq2d 6850 |
. . . . . . . 8
β’ (π§ = πΆ β (πβ(π§ β {π₯})) = (πβ(πΆ β {π₯}))) |
12 | 11 | eleq2d 2820 |
. . . . . . 7
β’ (π§ = πΆ β (π₯ β (πβ(π§ β {π₯})) β π₯ β (πβ(πΆ β {π₯})))) |
13 | 12 | notbid 318 |
. . . . . 6
β’ (π§ = πΆ β (Β¬ π₯ β (πβ(π§ β {π₯})) β Β¬ π₯ β (πβ(πΆ β {π₯})))) |
14 | 13 | raleqbi1dv 3306 |
. . . . 5
β’ (π§ = πΆ β (βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯})) β βπ₯ β πΆ Β¬ π₯ β (πβ(πΆ β {π₯})))) |
15 | 9, 14 | anbi12d 632 |
. . . 4
β’ (π§ = πΆ β ((πΆ β π§ β§ βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯}))) β (πΆ β πΆ β§ βπ₯ β πΆ Β¬ π₯ β (πβ(πΆ β {π₯}))))) |
16 | | lbsext.s |
. . . 4
β’ π = {π§ β π« π β£ (πΆ β π§ β§ βπ₯ β π§ Β¬ π₯ β (πβ(π§ β {π₯})))} |
17 | 15, 16 | elrab2 3652 |
. . 3
β’ (πΆ β π β (πΆ β π« π β§ (πΆ β πΆ β§ βπ₯ β πΆ Β¬ π₯ β (πβ(πΆ β {π₯}))))) |
18 | 5, 8, 17 | sylanbrc 584 |
. 2
β’ (π β πΆ β π) |
19 | 18 | ne0d 4299 |
1
β’ (π β π β β
) |