Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β§ (π‘ β π« π«
π β§ (toIncβπ‘) β Dirset)) β πΆ β (Mooreβπ)) |
2 | | elpwi 4571 |
. . . . . . . 8
β’ (π‘ β π« π«
π β π‘ β π« π) |
3 | 2 | ad2antrl 727 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β§ (π‘ β π« π«
π β§ (toIncβπ‘) β Dirset)) β π‘ β π« π) |
4 | | acsdrscl.f |
. . . . . . . 8
β’ πΉ = (mrClsβπΆ) |
5 | 4 | mrcuni 17509 |
. . . . . . 7
β’ ((πΆ β (Mooreβπ) β§ π‘ β π« π) β (πΉββͺ π‘) = (πΉββͺ (πΉ β π‘))) |
6 | 1, 3, 5 | syl2anc 585 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β§ (π‘ β π« π«
π β§ (toIncβπ‘) β Dirset)) β (πΉββͺ π‘) =
(πΉββͺ (πΉ
β π‘))) |
7 | 4 | mrcf 17497 |
. . . . . . . . . . . 12
β’ (πΆ β (Mooreβπ) β πΉ:π« πβΆπΆ) |
8 | 7 | ffnd 6673 |
. . . . . . . . . . 11
β’ (πΆ β (Mooreβπ) β πΉ Fn π« π) |
9 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((πΆ β (Mooreβπ) β§ (π‘ β π« π« π β§ (toIncβπ‘) β Dirset)) β πΉ Fn π« π) |
10 | | simpll 766 |
. . . . . . . . . . 11
β’ (((πΆ β (Mooreβπ) β§ (π‘ β π« π« π β§ (toIncβπ‘) β Dirset)) β§ (π₯ β π¦ β§ π¦ β π)) β πΆ β (Mooreβπ)) |
11 | | simprl 770 |
. . . . . . . . . . 11
β’ (((πΆ β (Mooreβπ) β§ (π‘ β π« π« π β§ (toIncβπ‘) β Dirset)) β§ (π₯ β π¦ β§ π¦ β π)) β π₯ β π¦) |
12 | | simprr 772 |
. . . . . . . . . . 11
β’ (((πΆ β (Mooreβπ) β§ (π‘ β π« π« π β§ (toIncβπ‘) β Dirset)) β§ (π₯ β π¦ β§ π¦ β π)) β π¦ β π) |
13 | 10, 4, 11, 12 | mrcssd 17512 |
. . . . . . . . . 10
β’ (((πΆ β (Mooreβπ) β§ (π‘ β π« π« π β§ (toIncβπ‘) β Dirset)) β§ (π₯ β π¦ β§ π¦ β π)) β (πΉβπ₯) β (πΉβπ¦)) |
14 | | simprr 772 |
. . . . . . . . . 10
β’ ((πΆ β (Mooreβπ) β§ (π‘ β π« π« π β§ (toIncβπ‘) β Dirset)) β (toIncβπ‘) β
Dirset) |
15 | 2 | ad2antrl 727 |
. . . . . . . . . 10
β’ ((πΆ β (Mooreβπ) β§ (π‘ β π« π« π β§ (toIncβπ‘) β Dirset)) β π‘ β π« π) |
16 | 4 | fvexi 6860 |
. . . . . . . . . . . 12
β’ πΉ β V |
17 | 16 | imaex 7857 |
. . . . . . . . . . 11
β’ (πΉ β π‘) β V |
18 | 17 | a1i 11 |
. . . . . . . . . 10
β’ ((πΆ β (Mooreβπ) β§ (π‘ β π« π« π β§ (toIncβπ‘) β Dirset)) β (πΉ β π‘) β V) |
19 | 9, 13, 14, 15, 18 | ipodrsima 18438 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ (π‘ β π« π« π β§ (toIncβπ‘) β Dirset)) β (toIncβ(πΉ β π‘)) β Dirset) |
20 | 19 | adantlr 714 |
. . . . . . . 8
β’ (((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β§ (π‘ β π« π«
π β§ (toIncβπ‘) β Dirset)) β
(toIncβ(πΉ β
π‘)) β
Dirset) |
21 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = (πΉ β π‘) β (toIncβπ ) = (toIncβ(πΉ β π‘))) |
22 | 21 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = (πΉ β π‘) β ((toIncβπ ) β Dirset β (toIncβ(πΉ β π‘)) β Dirset)) |
23 | | unieq 4880 |
. . . . . . . . . . 11
β’ (π = (πΉ β π‘) β βͺ π = βͺ
(πΉ β π‘)) |
24 | 23 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π = (πΉ β π‘) β (βͺ π β πΆ β βͺ (πΉ β π‘) β πΆ)) |
25 | 22, 24 | imbi12d 345 |
. . . . . . . . 9
β’ (π = (πΉ β π‘) β (((toIncβπ ) β Dirset β βͺ π
β πΆ) β
((toIncβ(πΉ β
π‘)) β Dirset β
βͺ (πΉ β π‘) β πΆ))) |
26 | | simplr 768 |
. . . . . . . . 9
β’ (((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β§ (π‘ β π« π«
π β§ (toIncβπ‘) β Dirset)) β
βπ β π«
πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) |
27 | | imassrn 6028 |
. . . . . . . . . . . 12
β’ (πΉ β π‘) β ran πΉ |
28 | 7 | frnd 6680 |
. . . . . . . . . . . 12
β’ (πΆ β (Mooreβπ) β ran πΉ β πΆ) |
29 | 27, 28 | sstrid 3959 |
. . . . . . . . . . 11
β’ (πΆ β (Mooreβπ) β (πΉ β π‘) β πΆ) |
30 | 17 | elpw 4568 |
. . . . . . . . . . 11
β’ ((πΉ β π‘) β π« πΆ β (πΉ β π‘) β πΆ) |
31 | 29, 30 | sylibr 233 |
. . . . . . . . . 10
β’ (πΆ β (Mooreβπ) β (πΉ β π‘) β π« πΆ) |
32 | 31 | ad2antrr 725 |
. . . . . . . . 9
β’ (((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β§ (π‘ β π« π«
π β§ (toIncβπ‘) β Dirset)) β (πΉ β π‘) β π« πΆ) |
33 | 25, 26, 32 | rspcdva 3584 |
. . . . . . . 8
β’ (((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β§ (π‘ β π« π«
π β§ (toIncβπ‘) β Dirset)) β
((toIncβ(πΉ β
π‘)) β Dirset β
βͺ (πΉ β π‘) β πΆ)) |
34 | 20, 33 | mpd 15 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β§ (π‘ β π« π«
π β§ (toIncβπ‘) β Dirset)) β βͺ (πΉ
β π‘) β πΆ) |
35 | 4 | mrcid 17501 |
. . . . . . 7
β’ ((πΆ β (Mooreβπ) β§ βͺ (πΉ
β π‘) β πΆ) β (πΉββͺ (πΉ β π‘)) = βͺ (πΉ β π‘)) |
36 | 1, 34, 35 | syl2anc 585 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β§ (π‘ β π« π«
π β§ (toIncβπ‘) β Dirset)) β (πΉββͺ (πΉ
β π‘)) = βͺ (πΉ
β π‘)) |
37 | 6, 36 | eqtrd 2773 |
. . . . 5
β’ (((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β§ (π‘ β π« π«
π β§ (toIncβπ‘) β Dirset)) β (πΉββͺ π‘) =
βͺ (πΉ β π‘)) |
38 | 37 | exp32 422 |
. . . 4
β’ ((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β (π‘ β π« π«
π β
((toIncβπ‘) β
Dirset β (πΉββͺ π‘) = βͺ
(πΉ β π‘)))) |
39 | 38 | ralrimiv 3139 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β
βπ‘ β π«
π« π((toIncβπ‘) β Dirset β (πΉββͺ π‘) = βͺ
(πΉ β π‘))) |
40 | 39 | ex 414 |
. 2
β’ (πΆ β (Mooreβπ) β (βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ) β
βπ‘ β π«
π« π((toIncβπ‘) β Dirset β (πΉββͺ π‘) = βͺ
(πΉ β π‘)))) |
41 | 40 | imdistani 570 |
1
β’ ((πΆ β (Mooreβπ) β§ βπ β π« πΆ((toIncβπ ) β Dirset β βͺ π
β πΆ)) β (πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘)))) |