Step | Hyp | Ref
| Expression |
1 | | n0i 4294 |
. . . 4
β’ (π β π΄ β Β¬ π΄ = β
) |
2 | | atombase.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
3 | 2 | eqeq1i 2738 |
. . . 4
β’ (π΄ = β
β
(AtomsβπΎ) =
β
) |
4 | 1, 3 | sylnib 328 |
. . 3
β’ (π β π΄ β Β¬ (AtomsβπΎ) = β
) |
5 | | fvprc 6835 |
. . 3
β’ (Β¬
πΎ β V β
(AtomsβπΎ) =
β
) |
6 | 4, 5 | nsyl2 141 |
. 2
β’ (π β π΄ β πΎ β V) |
7 | | atombase.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
8 | | eqid 2733 |
. . . 4
β’
(0.βπΎ) =
(0.βπΎ) |
9 | | eqid 2733 |
. . . 4
β’ ( β
βπΎ) = ( β
βπΎ) |
10 | 7, 8, 9, 2 | isat 37794 |
. . 3
β’ (πΎ β V β (π β π΄ β (π β π΅ β§ (0.βπΎ)( β βπΎ)π))) |
11 | 10 | simprbda 500 |
. 2
β’ ((πΎ β V β§ π β π΄) β π β π΅) |
12 | 6, 11 | mpancom 687 |
1
β’ (π β π΄ β π β π΅) |