Step | Hyp | Ref
| Expression |
1 | | elpwi 4568 |
. . . . 5
β’ (π β π« π β π β π) |
2 | | ralss 4015 |
. . . . . 6
β’ (π β π β (βπ β π βπ β π πΈ β π β βπ β π (π β π β βπ β π πΈ β π))) |
3 | | ralss 4015 |
. . . . . . . 8
β’ (π β π β (βπ β π (π β π β πΈ β π) β βπ β π (π β π β (π β π β πΈ β π)))) |
4 | | r19.21v 3173 |
. . . . . . . 8
β’
(βπ β
π (π β π β πΈ β π) β (π β π β βπ β π πΈ β π)) |
5 | | impexp 452 |
. . . . . . . . . 10
β’ (((π β π β§ π β π) β πΈ β π) β (π β π β (π β π β πΈ β π))) |
6 | | vex 3448 |
. . . . . . . . . . . 12
β’ π β V |
7 | | vex 3448 |
. . . . . . . . . . . 12
β’ π β V |
8 | 6, 7 | prss 4781 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β {π, π} β π) |
9 | 8 | imbi1i 350 |
. . . . . . . . . 10
β’ (((π β π β§ π β π) β πΈ β π) β ({π, π} β π β πΈ β π)) |
10 | 5, 9 | bitr3i 277 |
. . . . . . . . 9
β’ ((π β π β (π β π β πΈ β π)) β ({π, π} β π β πΈ β π)) |
11 | 10 | ralbii 3093 |
. . . . . . . 8
β’
(βπ β
π (π β π β (π β π β πΈ β π)) β βπ β π ({π, π} β π β πΈ β π)) |
12 | 3, 4, 11 | 3bitr3g 313 |
. . . . . . 7
β’ (π β π β ((π β π β βπ β π πΈ β π) β βπ β π ({π, π} β π β πΈ β π))) |
13 | 12 | ralbidv 3171 |
. . . . . 6
β’ (π β π β (βπ β π (π β π β βπ β π πΈ β π) β βπ β π βπ β π ({π, π} β π β πΈ β π))) |
14 | 2, 13 | bitrd 279 |
. . . . 5
β’ (π β π β (βπ β π βπ β π πΈ β π β βπ β π βπ β π ({π, π} β π β πΈ β π))) |
15 | 1, 14 | syl 17 |
. . . 4
β’ (π β π« π β (βπ β π βπ β π πΈ β π β βπ β π βπ β π ({π, π} β π β πΈ β π))) |
16 | 15 | rabbiia 3410 |
. . 3
β’ {π β π« π β£ βπ β π βπ β π πΈ β π} = {π β π« π β£ βπ β π βπ β π ({π, π} β π β πΈ β π)} |
17 | | riinrab 5045 |
. . 3
β’
(π« π β©
β© π β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)}) = {π β π« π β£ βπ β π βπ β π ({π, π} β π β πΈ β π)} |
18 | 16, 17 | eqtr4i 2764 |
. 2
β’ {π β π« π β£ βπ β π βπ β π πΈ β π} = (π« π β© β©
π β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)}) |
19 | | mreacs 17543 |
. . 3
β’ (π β π β (ACSβπ) β (Mooreβπ« π)) |
20 | | riinrab 5045 |
. . . . . . 7
β’
(π« π β©
β© π β π {π β π« π β£ ({π, π} β π β πΈ β π)}) = {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} |
21 | 19 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β π β§ π β π) β§ βπ β π πΈ β π) β (ACSβπ) β (Mooreβπ« π)) |
22 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β π) β§ (π β π β§ πΈ β π)) β π β π) |
23 | | simprr 772 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β π) β§ (π β π β§ πΈ β π)) β πΈ β π) |
24 | | prssi 4782 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β {π, π} β π) |
25 | 24 | ancoms 460 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π) β {π, π} β π) |
26 | 25 | ad2ant2lr 747 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β π) β§ (π β π β§ πΈ β π)) β {π, π} β π) |
27 | | prfi 9269 |
. . . . . . . . . . . . 13
β’ {π, π} β Fin |
28 | 27 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β π) β§ (π β π β§ πΈ β π)) β {π, π} β Fin) |
29 | | acsfn 17544 |
. . . . . . . . . . . 12
β’ (((π β π β§ πΈ β π) β§ ({π, π} β π β§ {π, π} β Fin)) β {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ)) |
30 | 22, 23, 26, 28, 29 | syl22anc 838 |
. . . . . . . . . . 11
β’ (((π β π β§ π β π) β§ (π β π β§ πΈ β π)) β {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ)) |
31 | 30 | expr 458 |
. . . . . . . . . 10
β’ (((π β π β§ π β π) β§ π β π) β (πΈ β π β {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ))) |
32 | 31 | ralimdva 3161 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β (βπ β π πΈ β π β βπ β π {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ))) |
33 | 32 | imp 408 |
. . . . . . . 8
β’ (((π β π β§ π β π) β§ βπ β π πΈ β π) β βπ β π {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ)) |
34 | | mreriincl 17483 |
. . . . . . . 8
β’
(((ACSβπ)
β (Mooreβπ« π) β§ βπ β π {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ)) β (π« π β© β©
π β π {π β π« π β£ ({π, π} β π β πΈ β π)}) β (ACSβπ)) |
35 | 21, 33, 34 | syl2anc 585 |
. . . . . . 7
β’ (((π β π β§ π β π) β§ βπ β π πΈ β π) β (π« π β© β©
π β π {π β π« π β£ ({π, π} β π β πΈ β π)}) β (ACSβπ)) |
36 | 20, 35 | eqeltrrid 2839 |
. . . . . 6
β’ (((π β π β§ π β π) β§ βπ β π πΈ β π) β {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} β (ACSβπ)) |
37 | 36 | ex 414 |
. . . . 5
β’ ((π β π β§ π β π) β (βπ β π πΈ β π β {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} β (ACSβπ))) |
38 | 37 | ralimdva 3161 |
. . . 4
β’ (π β π β (βπ β π βπ β π πΈ β π β βπ β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} β (ACSβπ))) |
39 | 38 | imp 408 |
. . 3
β’ ((π β π β§ βπ β π βπ β π πΈ β π) β βπ β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} β (ACSβπ)) |
40 | | mreriincl 17483 |
. . 3
β’
(((ACSβπ)
β (Mooreβπ« π) β§ βπ β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} β (ACSβπ)) β (π« π β© β©
π β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)}) β (ACSβπ)) |
41 | 19, 39, 40 | syl2an2r 684 |
. 2
β’ ((π β π β§ βπ β π βπ β π πΈ β π) β (π« π β© β©
π β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)}) β (ACSβπ)) |
42 | 18, 41 | eqeltrid 2838 |
1
β’ ((π β π β§ βπ β π βπ β π πΈ β π) β {π β π« π β£ βπ β π βπ β π πΈ β π} β (ACSβπ)) |