Step | Hyp | Ref
| Expression |
1 | | islnopp.a |
. . 3
β’ (π β π΄ β π) |
2 | | islnopp.b |
. . 3
β’ (π β π΅ β π) |
3 | | eleq1 2822 |
. . . . . 6
β’ (π’ = π΄ β (π’ β (π β π·) β π΄ β (π β π·))) |
4 | 3 | anbi1d 631 |
. . . . 5
β’ (π’ = π΄ β ((π’ β (π β π·) β§ π£ β (π β π·)) β (π΄ β (π β π·) β§ π£ β (π β π·)))) |
5 | | oveq1 7416 |
. . . . . . 7
β’ (π’ = π΄ β (π’πΌπ£) = (π΄πΌπ£)) |
6 | 5 | eleq2d 2820 |
. . . . . 6
β’ (π’ = π΄ β (π‘ β (π’πΌπ£) β π‘ β (π΄πΌπ£))) |
7 | 6 | rexbidv 3179 |
. . . . 5
β’ (π’ = π΄ β (βπ‘ β π· π‘ β (π’πΌπ£) β βπ‘ β π· π‘ β (π΄πΌπ£))) |
8 | 4, 7 | anbi12d 632 |
. . . 4
β’ (π’ = π΄ β (((π’ β (π β π·) β§ π£ β (π β π·)) β§ βπ‘ β π· π‘ β (π’πΌπ£)) β ((π΄ β (π β π·) β§ π£ β (π β π·)) β§ βπ‘ β π· π‘ β (π΄πΌπ£)))) |
9 | | eleq1 2822 |
. . . . . 6
β’ (π£ = π΅ β (π£ β (π β π·) β π΅ β (π β π·))) |
10 | 9 | anbi2d 630 |
. . . . 5
β’ (π£ = π΅ β ((π΄ β (π β π·) β§ π£ β (π β π·)) β (π΄ β (π β π·) β§ π΅ β (π β π·)))) |
11 | | oveq2 7417 |
. . . . . . 7
β’ (π£ = π΅ β (π΄πΌπ£) = (π΄πΌπ΅)) |
12 | 11 | eleq2d 2820 |
. . . . . 6
β’ (π£ = π΅ β (π‘ β (π΄πΌπ£) β π‘ β (π΄πΌπ΅))) |
13 | 12 | rexbidv 3179 |
. . . . 5
β’ (π£ = π΅ β (βπ‘ β π· π‘ β (π΄πΌπ£) β βπ‘ β π· π‘ β (π΄πΌπ΅))) |
14 | 10, 13 | anbi12d 632 |
. . . 4
β’ (π£ = π΅ β (((π΄ β (π β π·) β§ π£ β (π β π·)) β§ βπ‘ β π· π‘ β (π΄πΌπ£)) β ((π΄ β (π β π·) β§ π΅ β (π β π·)) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)))) |
15 | | hpg.o |
. . . . 5
β’ π = {β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} |
16 | | simpl 484 |
. . . . . . . . 9
β’ ((π = π’ β§ π = π£) β π = π’) |
17 | 16 | eleq1d 2819 |
. . . . . . . 8
β’ ((π = π’ β§ π = π£) β (π β (π β π·) β π’ β (π β π·))) |
18 | | simpr 486 |
. . . . . . . . 9
β’ ((π = π’ β§ π = π£) β π = π£) |
19 | 18 | eleq1d 2819 |
. . . . . . . 8
β’ ((π = π’ β§ π = π£) β (π β (π β π·) β π£ β (π β π·))) |
20 | 17, 19 | anbi12d 632 |
. . . . . . 7
β’ ((π = π’ β§ π = π£) β ((π β (π β π·) β§ π β (π β π·)) β (π’ β (π β π·) β§ π£ β (π β π·)))) |
21 | | oveq12 7418 |
. . . . . . . . 9
β’ ((π = π’ β§ π = π£) β (ππΌπ) = (π’πΌπ£)) |
22 | 21 | eleq2d 2820 |
. . . . . . . 8
β’ ((π = π’ β§ π = π£) β (π‘ β (ππΌπ) β π‘ β (π’πΌπ£))) |
23 | 22 | rexbidv 3179 |
. . . . . . 7
β’ ((π = π’ β§ π = π£) β (βπ‘ β π· π‘ β (ππΌπ) β βπ‘ β π· π‘ β (π’πΌπ£))) |
24 | 20, 23 | anbi12d 632 |
. . . . . 6
β’ ((π = π’ β§ π = π£) β (((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ)) β ((π’ β (π β π·) β§ π£ β (π β π·)) β§ βπ‘ β π· π‘ β (π’πΌπ£)))) |
25 | 24 | cbvopabv 5222 |
. . . . 5
β’
{β¨π, πβ© β£ ((π β (π β π·) β§ π β (π β π·)) β§ βπ‘ β π· π‘ β (ππΌπ))} = {β¨π’, π£β© β£ ((π’ β (π β π·) β§ π£ β (π β π·)) β§ βπ‘ β π· π‘ β (π’πΌπ£))} |
26 | 15, 25 | eqtri 2761 |
. . . 4
β’ π = {β¨π’, π£β© β£ ((π’ β (π β π·) β§ π£ β (π β π·)) β§ βπ‘ β π· π‘ β (π’πΌπ£))} |
27 | 8, 14, 26 | brabg 5540 |
. . 3
β’ ((π΄ β π β§ π΅ β π) β (π΄ππ΅ β ((π΄ β (π β π·) β§ π΅ β (π β π·)) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)))) |
28 | 1, 2, 27 | syl2anc 585 |
. 2
β’ (π β (π΄ππ΅ β ((π΄ β (π β π·) β§ π΅ β (π β π·)) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)))) |
29 | 1 | biantrurd 534 |
. . . . 5
β’ (π β (Β¬ π΄ β π· β (π΄ β π β§ Β¬ π΄ β π·))) |
30 | | eldif 3959 |
. . . . 5
β’ (π΄ β (π β π·) β (π΄ β π β§ Β¬ π΄ β π·)) |
31 | 29, 30 | bitr4di 289 |
. . . 4
β’ (π β (Β¬ π΄ β π· β π΄ β (π β π·))) |
32 | 2 | biantrurd 534 |
. . . . 5
β’ (π β (Β¬ π΅ β π· β (π΅ β π β§ Β¬ π΅ β π·))) |
33 | | eldif 3959 |
. . . . 5
β’ (π΅ β (π β π·) β (π΅ β π β§ Β¬ π΅ β π·)) |
34 | 32, 33 | bitr4di 289 |
. . . 4
β’ (π β (Β¬ π΅ β π· β π΅ β (π β π·))) |
35 | 31, 34 | anbi12d 632 |
. . 3
β’ (π β ((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β (π΄ β (π β π·) β§ π΅ β (π β π·)))) |
36 | 35 | anbi1d 631 |
. 2
β’ (π β (((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)) β ((π΄ β (π β π·) β§ π΅ β (π β π·)) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)))) |
37 | 28, 36 | bitr4d 282 |
1
β’ (π β (π΄ππ΅ β ((Β¬ π΄ β π· β§ Β¬ π΅ β π·) β§ βπ‘ β π· π‘ β (π΄πΌπ΅)))) |