Step | Hyp | Ref
| Expression |
1 | | irred.4 |
. . . . . . 7
β’ π = (π΅ β π) |
2 | 1 | eleq2i 2828 |
. . . . . 6
β’ (π β π β π β (π΅ β π)) |
3 | | eldif 3908 |
. . . . . 6
β’ (π β (π΅ β π) β (π β π΅ β§ Β¬ π β π)) |
4 | 2, 3 | bitri 274 |
. . . . 5
β’ (π β π β (π β π΅ β§ Β¬ π β π)) |
5 | 4 | baibr 537 |
. . . 4
β’ (π β π΅ β (Β¬ π β π β π β π)) |
6 | | df-ne 2941 |
. . . . . . . . 9
β’ ((π₯ Β· π¦) β π β Β¬ (π₯ Β· π¦) = π) |
7 | 6 | ralbii 3092 |
. . . . . . . 8
β’
(βπ¦ β
π (π₯ Β· π¦) β π β βπ¦ β π Β¬ (π₯ Β· π¦) = π) |
8 | | ralnex 3072 |
. . . . . . . 8
β’
(βπ¦ β
π Β¬ (π₯ Β· π¦) = π β Β¬ βπ¦ β π (π₯ Β· π¦) = π) |
9 | 7, 8 | bitri 274 |
. . . . . . 7
β’
(βπ¦ β
π (π₯ Β· π¦) β π β Β¬ βπ¦ β π (π₯ Β· π¦) = π) |
10 | 9 | ralbii 3092 |
. . . . . 6
β’
(βπ₯ β
π βπ¦ β π (π₯ Β· π¦) β π β βπ₯ β π Β¬ βπ¦ β π (π₯ Β· π¦) = π) |
11 | | ralnex 3072 |
. . . . . 6
β’
(βπ₯ β
π Β¬ βπ¦ β π (π₯ Β· π¦) = π β Β¬ βπ₯ β π βπ¦ β π (π₯ Β· π¦) = π) |
12 | 10, 11 | bitr2i 275 |
. . . . 5
β’ (Β¬
βπ₯ β π βπ¦ β π (π₯ Β· π¦) = π β βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π) |
13 | 12 | a1i 11 |
. . . 4
β’ (π β π΅ β (Β¬ βπ₯ β π βπ¦ β π (π₯ Β· π¦) = π β βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π)) |
14 | 5, 13 | anbi12d 631 |
. . 3
β’ (π β π΅ β ((Β¬ π β π β§ Β¬ βπ₯ β π βπ¦ β π (π₯ Β· π¦) = π) β (π β π β§ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π))) |
15 | | ioran 981 |
. . 3
β’ (Β¬
(π β π β¨ βπ₯ β π βπ¦ β π (π₯ Β· π¦) = π) β (Β¬ π β π β§ Β¬ βπ₯ β π βπ¦ β π (π₯ Β· π¦) = π)) |
16 | | irred.1 |
. . . 4
β’ π΅ = (Baseβπ
) |
17 | | irred.2 |
. . . 4
β’ π = (Unitβπ
) |
18 | | irred.3 |
. . . 4
β’ πΌ = (Irredβπ
) |
19 | | irred.5 |
. . . 4
β’ Β· =
(.rβπ
) |
20 | 16, 17, 18, 1, 19 | isirred 20036 |
. . 3
β’ (π β πΌ β (π β π β§ βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π)) |
21 | 14, 15, 20 | 3bitr4g 313 |
. 2
β’ (π β π΅ β (Β¬ (π β π β¨ βπ₯ β π βπ¦ β π (π₯ Β· π¦) = π) β π β πΌ)) |
22 | 21 | con1bid 355 |
1
β’ (π β π΅ β (Β¬ π β πΌ β (π β π β¨ βπ₯ β π βπ¦ β π (π₯ Β· π¦) = π))) |