Step | Hyp | Ref
| Expression |
1 | | elpwi 4609 |
. . . . 5
β’ (π β π« π β π β π) |
2 | | ralss 4054 |
. . . . . 6
β’ (π β π β (βπ β π βπ β π πΈ β π β βπ β π (π β π β βπ β π πΈ β π))) |
3 | | ralss 4054 |
. . . . . . . 8
β’ (π β π β (βπ β π (π β π β πΈ β π) β βπ β π (π β π β (π β π β πΈ β π)))) |
4 | | r19.21v 3179 |
. . . . . . . 8
β’
(βπ β
π (π β π β πΈ β π) β (π β π β βπ β π πΈ β π)) |
5 | | impexp 451 |
. . . . . . . . . 10
β’ (((π β π β§ π β π) β πΈ β π) β (π β π β (π β π β πΈ β π))) |
6 | | vex 3478 |
. . . . . . . . . . . 12
β’ π β V |
7 | | vex 3478 |
. . . . . . . . . . . 12
β’ π β V |
8 | 6, 7 | prss 4823 |
. . . . . . . . . . 11
β’ ((π β π β§ π β π) β {π, π} β π) |
9 | 8 | imbi1i 349 |
. . . . . . . . . 10
β’ (((π β π β§ π β π) β πΈ β π) β ({π, π} β π β πΈ β π)) |
10 | 5, 9 | bitr3i 276 |
. . . . . . . . 9
β’ ((π β π β (π β π β πΈ β π)) β ({π, π} β π β πΈ β π)) |
11 | 10 | ralbii 3093 |
. . . . . . . 8
β’
(βπ β
π (π β π β (π β π β πΈ β π)) β βπ β π ({π, π} β π β πΈ β π)) |
12 | 3, 4, 11 | 3bitr3g 312 |
. . . . . . 7
β’ (π β π β ((π β π β βπ β π πΈ β π) β βπ β π ({π, π} β π β πΈ β π))) |
13 | 12 | ralbidv 3177 |
. . . . . 6
β’ (π β π β (βπ β π (π β π β βπ β π πΈ β π) β βπ β π βπ β π ({π, π} β π β πΈ β π))) |
14 | 2, 13 | bitrd 278 |
. . . . 5
β’ (π β π β (βπ β π βπ β π πΈ β π β βπ β π βπ β π ({π, π} β π β πΈ β π))) |
15 | 1, 14 | syl 17 |
. . . 4
β’ (π β π« π β (βπ β π βπ β π πΈ β π β βπ β π βπ β π ({π, π} β π β πΈ β π))) |
16 | 15 | rabbiia 3436 |
. . 3
β’ {π β π« π β£ βπ β π βπ β π πΈ β π} = {π β π« π β£ βπ β π βπ β π ({π, π} β π β πΈ β π)} |
17 | | riinrab 5087 |
. . 3
β’
(π« π β©
β© π β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)}) = {π β π« π β£ βπ β π βπ β π ({π, π} β π β πΈ β π)} |
18 | 16, 17 | eqtr4i 2763 |
. 2
β’ {π β π« π β£ βπ β π βπ β π πΈ β π} = (π« π β© β©
π β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)}) |
19 | | mreacs 17601 |
. . 3
β’ (π β π β (ACSβπ) β (Mooreβπ« π)) |
20 | | riinrab 5087 |
. . . . . . 7
β’
(π« π β©
β© π β π {π β π« π β£ ({π, π} β π β πΈ β π)}) = {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} |
21 | 19 | ad2antrr 724 |
. . . . . . . 8
β’ (((π β π β§ π β π) β§ βπ β π πΈ β π) β (ACSβπ) β (Mooreβπ« π)) |
22 | | simpll 765 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β π) β§ (π β π β§ πΈ β π)) β π β π) |
23 | | simprr 771 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β π) β§ (π β π β§ πΈ β π)) β πΈ β π) |
24 | | prssi 4824 |
. . . . . . . . . . . . . 14
β’ ((π β π β§ π β π) β {π, π} β π) |
25 | 24 | ancoms 459 |
. . . . . . . . . . . . 13
β’ ((π β π β§ π β π) β {π, π} β π) |
26 | 25 | ad2ant2lr 746 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β π) β§ (π β π β§ πΈ β π)) β {π, π} β π) |
27 | | prfi 9321 |
. . . . . . . . . . . . 13
β’ {π, π} β Fin |
28 | 27 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β π β§ π β π) β§ (π β π β§ πΈ β π)) β {π, π} β Fin) |
29 | | acsfn 17602 |
. . . . . . . . . . . 12
β’ (((π β π β§ πΈ β π) β§ ({π, π} β π β§ {π, π} β Fin)) β {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ)) |
30 | 22, 23, 26, 28, 29 | syl22anc 837 |
. . . . . . . . . . 11
β’ (((π β π β§ π β π) β§ (π β π β§ πΈ β π)) β {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ)) |
31 | 30 | expr 457 |
. . . . . . . . . 10
β’ (((π β π β§ π β π) β§ π β π) β (πΈ β π β {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ))) |
32 | 31 | ralimdva 3167 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β (βπ β π πΈ β π β βπ β π {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ))) |
33 | 32 | imp 407 |
. . . . . . . 8
β’ (((π β π β§ π β π) β§ βπ β π πΈ β π) β βπ β π {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ)) |
34 | | mreriincl 17541 |
. . . . . . . 8
β’
(((ACSβπ)
β (Mooreβπ« π) β§ βπ β π {π β π« π β£ ({π, π} β π β πΈ β π)} β (ACSβπ)) β (π« π β© β©
π β π {π β π« π β£ ({π, π} β π β πΈ β π)}) β (ACSβπ)) |
35 | 21, 33, 34 | syl2anc 584 |
. . . . . . 7
β’ (((π β π β§ π β π) β§ βπ β π πΈ β π) β (π« π β© β©
π β π {π β π« π β£ ({π, π} β π β πΈ β π)}) β (ACSβπ)) |
36 | 20, 35 | eqeltrrid 2838 |
. . . . . 6
β’ (((π β π β§ π β π) β§ βπ β π πΈ β π) β {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} β (ACSβπ)) |
37 | 36 | ex 413 |
. . . . 5
β’ ((π β π β§ π β π) β (βπ β π πΈ β π β {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} β (ACSβπ))) |
38 | 37 | ralimdva 3167 |
. . . 4
β’ (π β π β (βπ β π βπ β π πΈ β π β βπ β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} β (ACSβπ))) |
39 | 38 | imp 407 |
. . 3
β’ ((π β π β§ βπ β π βπ β π πΈ β π) β βπ β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} β (ACSβπ)) |
40 | | mreriincl 17541 |
. . 3
β’
(((ACSβπ)
β (Mooreβπ« π) β§ βπ β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)} β (ACSβπ)) β (π« π β© β©
π β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)}) β (ACSβπ)) |
41 | 19, 39, 40 | syl2an2r 683 |
. 2
β’ ((π β π β§ βπ β π βπ β π πΈ β π) β (π« π β© β©
π β π {π β π« π β£ βπ β π ({π, π} β π β πΈ β π)}) β (ACSβπ)) |
42 | 18, 41 | eqeltrid 2837 |
1
β’ ((π β π β§ βπ β π βπ β π πΈ β π) β {π β π« π β£ βπ β π βπ β π πΈ β π} β (ACSβπ)) |