Step | Hyp | Ref
| Expression |
1 | | neanior 3035 |
. . . 4
β’ ((π β β
β§ π β β
) β Β¬
(π = β
β¨ π = β
)) |
2 | 1 | bicomi 223 |
. . 3
β’ (Β¬
(π = β
β¨ π = β
) β (π β β
β§ π β β
)) |
3 | 2 | con1bii 356 |
. 2
β’ (Β¬
(π β β
β§ π β β
) β (π = β
β¨ π = β
)) |
4 | | eqid 2732 |
. . . 4
β’
(leβπΎ) =
(leβπΎ) |
5 | | eqid 2732 |
. . . 4
β’
(joinβπΎ) =
(joinβπΎ) |
6 | | padd0.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
7 | | padd0.p |
. . . 4
β’ + =
(+πβπΎ) |
8 | 4, 5, 6, 7 | elpadd 38973 |
. . 3
β’ ((πΎ β π΅ β§ π β π΄ β§ π β π΄) β (π β (π + π) β ((π β π β¨ π β π) β¨ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))))) |
9 | | rex0 4357 |
. . . . . . . 8
β’ Β¬
βπ β β
βπ β π π(leβπΎ)(π(joinβπΎ)π) |
10 | | rexeq 3321 |
. . . . . . . 8
β’ (π = β
β (βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π) β βπ β β
βπ β π π(leβπΎ)(π(joinβπΎ)π))) |
11 | 9, 10 | mtbiri 326 |
. . . . . . 7
β’ (π = β
β Β¬
βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)) |
12 | | rex0 4357 |
. . . . . . . . . 10
β’ Β¬
βπ β β
π(leβπΎ)(π(joinβπΎ)π) |
13 | 12 | a1i 11 |
. . . . . . . . 9
β’ (π β π β Β¬ βπ β β
π(leβπΎ)(π(joinβπΎ)π)) |
14 | 13 | nrex 3074 |
. . . . . . . 8
β’ Β¬
βπ β π βπ β β
π(leβπΎ)(π(joinβπΎ)π) |
15 | | rexeq 3321 |
. . . . . . . . 9
β’ (π = β
β (βπ β π π(leβπΎ)(π(joinβπΎ)π) β βπ β β
π(leβπΎ)(π(joinβπΎ)π))) |
16 | 15 | rexbidv 3178 |
. . . . . . . 8
β’ (π = β
β (βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π) β βπ β π βπ β β
π(leβπΎ)(π(joinβπΎ)π))) |
17 | 14, 16 | mtbiri 326 |
. . . . . . 7
β’ (π = β
β Β¬
βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)) |
18 | 11, 17 | jaoi 855 |
. . . . . 6
β’ ((π = β
β¨ π = β
) β Β¬
βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)) |
19 | 18 | intnand 489 |
. . . . 5
β’ ((π = β
β¨ π = β
) β Β¬ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))) |
20 | | biorf 935 |
. . . . 5
β’ (Β¬
(π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)) β ((π β π β¨ π β π) β ((π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)) β¨ (π β π β¨ π β π)))) |
21 | 19, 20 | syl 17 |
. . . 4
β’ ((π = β
β¨ π = β
) β ((π β π β¨ π β π) β ((π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)) β¨ (π β π β¨ π β π)))) |
22 | | orcom 868 |
. . . 4
β’ (((π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)) β¨ (π β π β¨ π β π)) β ((π β π β¨ π β π) β¨ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π)))) |
23 | 21, 22 | bitr2di 287 |
. . 3
β’ ((π = β
β¨ π = β
) β (((π β π β¨ π β π) β¨ (π β π΄ β§ βπ β π βπ β π π(leβπΎ)(π(joinβπΎ)π))) β (π β π β¨ π β π))) |
24 | 8, 23 | sylan9bb 510 |
. 2
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ (π = β
β¨ π = β
)) β (π β (π + π) β (π β π β¨ π β π))) |
25 | 3, 24 | sylan2b 594 |
1
β’ (((πΎ β π΅ β§ π β π΄ β§ π β π΄) β§ Β¬ (π β β
β§ π β β
)) β (π β (π + π) β (π β π β¨ π β π))) |