Step | Hyp | Ref
| Expression |
1 | | unifpw 9354 |
. . . . . 6
β’ βͺ (π« π β© Fin) = π |
2 | 1 | fveq2i 6894 |
. . . . 5
β’ (πΉββͺ (π« π β© Fin)) = (πΉβπ ) |
3 | | vex 3478 |
. . . . . . 7
β’ π β V |
4 | | fpwipodrs 18492 |
. . . . . . 7
β’ (π β V β
(toIncβ(π« π
β© Fin)) β Dirset) |
5 | 3, 4 | mp1i 13 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β (toIncβ(π« π β© Fin)) β
Dirset) |
6 | | fveq2 6891 |
. . . . . . . . 9
β’ (π‘ = (π« π β© Fin) β (toIncβπ‘) = (toIncβ(π«
π β©
Fin))) |
7 | 6 | eleq1d 2818 |
. . . . . . . 8
β’ (π‘ = (π« π β© Fin) β ((toIncβπ‘) β Dirset β
(toIncβ(π« π
β© Fin)) β Dirset)) |
8 | | unieq 4919 |
. . . . . . . . . 10
β’ (π‘ = (π« π β© Fin) β βͺ π‘ =
βͺ (π« π β© Fin)) |
9 | 8 | fveq2d 6895 |
. . . . . . . . 9
β’ (π‘ = (π« π β© Fin) β (πΉββͺ π‘) = (πΉββͺ
(π« π β©
Fin))) |
10 | | imaeq2 6055 |
. . . . . . . . . 10
β’ (π‘ = (π« π β© Fin) β (πΉ β π‘) = (πΉ β (π« π β© Fin))) |
11 | 10 | unieqd 4922 |
. . . . . . . . 9
β’ (π‘ = (π« π β© Fin) β βͺ (πΉ
β π‘) = βͺ (πΉ
β (π« π β©
Fin))) |
12 | 9, 11 | eqeq12d 2748 |
. . . . . . . 8
β’ (π‘ = (π« π β© Fin) β ((πΉββͺ π‘) = βͺ
(πΉ β π‘) β (πΉββͺ
(π« π β© Fin)) =
βͺ (πΉ β (π« π β© Fin)))) |
13 | 7, 12 | imbi12d 344 |
. . . . . . 7
β’ (π‘ = (π« π β© Fin) β (((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘)) β ((toIncβ(π« π β© Fin)) β Dirset
β (πΉββͺ (π« π β© Fin)) = βͺ
(πΉ β (π« π β© Fin))))) |
14 | | simplr 767 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β βπ‘ β π« π« π((toIncβπ‘) β Dirset β (πΉββͺ π‘) = βͺ
(πΉ β π‘))) |
15 | | inss1 4228 |
. . . . . . . . . 10
β’
(π« π β©
Fin) β π« π |
16 | | elpwi 4609 |
. . . . . . . . . . . 12
β’ (π β π« π β π β π) |
17 | 16 | sspwd 4615 |
. . . . . . . . . . 11
β’ (π β π« π β π« π β π« π) |
18 | 17 | adantl 482 |
. . . . . . . . . 10
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β π« π β π« π) |
19 | 15, 18 | sstrid 3993 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (π« π β© Fin) β π« π) |
20 | | vpwex 5375 |
. . . . . . . . . . 11
β’ π«
π β V |
21 | 20 | inex1 5317 |
. . . . . . . . . 10
β’
(π« π β©
Fin) β V |
22 | 21 | elpw 4606 |
. . . . . . . . 9
β’
((π« π β©
Fin) β π« π« π β (π« π β© Fin) β π« π) |
23 | 19, 22 | sylibr 233 |
. . . . . . . 8
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (π« π β© Fin) β π« π« π) |
24 | 23 | adantlr 713 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β (π« π β© Fin) β π« π« π) |
25 | 13, 14, 24 | rspcdva 3613 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β ((toIncβ(π« π β© Fin)) β Dirset
β (πΉββͺ (π« π β© Fin)) = βͺ
(πΉ β (π« π β© Fin)))) |
26 | 5, 25 | mpd 15 |
. . . . 5
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β (πΉββͺ
(π« π β© Fin)) =
βͺ (πΉ β (π« π β© Fin))) |
27 | 2, 26 | eqtr3id 2786 |
. . . 4
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β (πΉβπ ) = βͺ (πΉ β (π« π β© Fin))) |
28 | 27 | ralrimiva 3146 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β βπ β π« π(πΉβπ ) = βͺ (πΉ β (π« π β© Fin))) |
29 | 28 | ex 413 |
. 2
β’ (πΆ β (Mooreβπ) β (βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘)) β βπ β π« π(πΉβπ ) = βͺ (πΉ β (π« π β© Fin)))) |
30 | 29 | imdistani 569 |
1
β’ ((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β (πΆ β (Mooreβπ) β§ βπ β π« π(πΉβπ ) = βͺ (πΉ β (π« π β© Fin)))) |