Step | Hyp | Ref
| Expression |
1 | | fveqeq2 6851 |
. . . . 5
β’ (π₯ = π β ((π·βπ₯) = πΎ β (π·βπ) = πΎ)) |
2 | 1 | notbid 317 |
. . . 4
β’ (π₯ = π β (Β¬ (π·βπ₯) = πΎ β Β¬ (π·βπ) = πΎ)) |
3 | | frgrwopreg.b |
. . . . 5
β’ π΅ = (π β π΄) |
4 | | frgrwopreg.a |
. . . . . 6
β’ π΄ = {π₯ β π β£ (π·βπ₯) = πΎ} |
5 | 4 | difeq2i 4079 |
. . . . 5
β’ (π β π΄) = (π β {π₯ β π β£ (π·βπ₯) = πΎ}) |
6 | | notrab 4271 |
. . . . 5
β’ (π β {π₯ β π β£ (π·βπ₯) = πΎ}) = {π₯ β π β£ Β¬ (π·βπ₯) = πΎ} |
7 | 3, 5, 6 | 3eqtri 2768 |
. . . 4
β’ π΅ = {π₯ β π β£ Β¬ (π·βπ₯) = πΎ} |
8 | 2, 7 | elrab2 3648 |
. . 3
β’ (π β π΅ β (π β π β§ Β¬ (π·βπ) = πΎ)) |
9 | | fveqeq2 6851 |
. . . . . 6
β’ (π₯ = π β ((π·βπ₯) = πΎ β (π·βπ) = πΎ)) |
10 | 9, 4 | elrab2 3648 |
. . . . 5
β’ (π β π΄ β (π β π β§ (π·βπ) = πΎ)) |
11 | | eqeq2 2748 |
. . . . . . 7
β’ ((π·βπ) = πΎ β ((π·βπ) = (π·βπ) β (π·βπ) = πΎ)) |
12 | 11 | notbid 317 |
. . . . . 6
β’ ((π·βπ) = πΎ β (Β¬ (π·βπ) = (π·βπ) β Β¬ (π·βπ) = πΎ)) |
13 | | neqne 2951 |
. . . . . . 7
β’ (Β¬
(π·βπ) = (π·βπ) β (π·βπ) β (π·βπ)) |
14 | 13 | necomd 2999 |
. . . . . 6
β’ (Β¬
(π·βπ) = (π·βπ) β (π·βπ) β (π·βπ)) |
15 | 12, 14 | syl6bir 253 |
. . . . 5
β’ ((π·βπ) = πΎ β (Β¬ (π·βπ) = πΎ β (π·βπ) β (π·βπ))) |
16 | 10, 15 | simplbiim 505 |
. . . 4
β’ (π β π΄ β (Β¬ (π·βπ) = πΎ β (π·βπ) β (π·βπ))) |
17 | 16 | com12 32 |
. . 3
β’ (Β¬
(π·βπ) = πΎ β (π β π΄ β (π·βπ) β (π·βπ))) |
18 | 8, 17 | simplbiim 505 |
. 2
β’ (π β π΅ β (π β π΄ β (π·βπ) β (π·βπ))) |
19 | 18 | impcom 408 |
1
β’ ((π β π΄ β§ π β π΅) β (π·βπ) β (π·βπ)) |