Step | Hyp | Ref
| Expression |
1 | | unifpw 9305 |
. . . . . 6
β’ βͺ (π« π β© Fin) = π |
2 | 1 | fveq2i 6849 |
. . . . 5
β’ (πΉββͺ (π« π β© Fin)) = (πΉβπ ) |
3 | | vex 3451 |
. . . . . . 7
β’ π β V |
4 | | fpwipodrs 18437 |
. . . . . . 7
β’ (π β V β
(toIncβ(π« π
β© Fin)) β Dirset) |
5 | 3, 4 | mp1i 13 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β (toIncβ(π« π β© Fin)) β
Dirset) |
6 | | fveq2 6846 |
. . . . . . . . 9
β’ (π‘ = (π« π β© Fin) β (toIncβπ‘) = (toIncβ(π«
π β©
Fin))) |
7 | 6 | eleq1d 2819 |
. . . . . . . 8
β’ (π‘ = (π« π β© Fin) β ((toIncβπ‘) β Dirset β
(toIncβ(π« π
β© Fin)) β Dirset)) |
8 | | unieq 4880 |
. . . . . . . . . 10
β’ (π‘ = (π« π β© Fin) β βͺ π‘ =
βͺ (π« π β© Fin)) |
9 | 8 | fveq2d 6850 |
. . . . . . . . 9
β’ (π‘ = (π« π β© Fin) β (πΉββͺ π‘) = (πΉββͺ
(π« π β©
Fin))) |
10 | | imaeq2 6013 |
. . . . . . . . . 10
β’ (π‘ = (π« π β© Fin) β (πΉ β π‘) = (πΉ β (π« π β© Fin))) |
11 | 10 | unieqd 4883 |
. . . . . . . . 9
β’ (π‘ = (π« π β© Fin) β βͺ (πΉ
β π‘) = βͺ (πΉ
β (π« π β©
Fin))) |
12 | 9, 11 | eqeq12d 2749 |
. . . . . . . 8
β’ (π‘ = (π« π β© Fin) β ((πΉββͺ π‘) = βͺ
(πΉ β π‘) β (πΉββͺ
(π« π β© Fin)) =
βͺ (πΉ β (π« π β© Fin)))) |
13 | 7, 12 | imbi12d 345 |
. . . . . . 7
β’ (π‘ = (π« π β© Fin) β (((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘)) β ((toIncβ(π« π β© Fin)) β Dirset
β (πΉββͺ (π« π β© Fin)) = βͺ
(πΉ β (π« π β© Fin))))) |
14 | | simplr 768 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β βπ‘ β π« π« π((toIncβπ‘) β Dirset β (πΉββͺ π‘) = βͺ
(πΉ β π‘))) |
15 | | inss1 4192 |
. . . . . . . . . 10
β’
(π« π β©
Fin) β π« π |
16 | | elpwi 4571 |
. . . . . . . . . . . 12
β’ (π β π« π β π β π) |
17 | 16 | sspwd 4577 |
. . . . . . . . . . 11
β’ (π β π« π β π« π β π« π) |
18 | 17 | adantl 483 |
. . . . . . . . . 10
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β π« π β π« π) |
19 | 15, 18 | sstrid 3959 |
. . . . . . . . 9
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (π« π β© Fin) β π« π) |
20 | | vpwex 5336 |
. . . . . . . . . . 11
β’ π«
π β V |
21 | 20 | inex1 5278 |
. . . . . . . . . 10
β’
(π« π β©
Fin) β V |
22 | 21 | elpw 4568 |
. . . . . . . . 9
β’
((π« π β©
Fin) β π« π« π β (π« π β© Fin) β π« π) |
23 | 19, 22 | sylibr 233 |
. . . . . . . 8
β’ ((πΆ β (Mooreβπ) β§ π β π« π) β (π« π β© Fin) β π« π« π) |
24 | 23 | adantlr 714 |
. . . . . . 7
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β (π« π β© Fin) β π« π« π) |
25 | 13, 14, 24 | rspcdva 3584 |
. . . . . 6
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β ((toIncβ(π« π β© Fin)) β Dirset
β (πΉββͺ (π« π β© Fin)) = βͺ
(πΉ β (π« π β© Fin)))) |
26 | 5, 25 | mpd 15 |
. . . . 5
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β (πΉββͺ
(π« π β© Fin)) =
βͺ (πΉ β (π« π β© Fin))) |
27 | 2, 26 | eqtr3id 2787 |
. . . 4
β’ (((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β§ π β π« π) β (πΉβπ ) = βͺ (πΉ β (π« π β© Fin))) |
28 | 27 | ralrimiva 3140 |
. . 3
β’ ((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β βπ β π« π(πΉβπ ) = βͺ (πΉ β (π« π β© Fin))) |
29 | 28 | ex 414 |
. 2
β’ (πΆ β (Mooreβπ) β (βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘)) β βπ β π« π(πΉβπ ) = βͺ (πΉ β (π« π β© Fin)))) |
30 | 29 | imdistani 570 |
1
β’ ((πΆ β (Mooreβπ) β§ βπ‘ β π« π«
π((toIncβπ‘) β Dirset β (πΉββͺ π‘) =
βͺ (πΉ β π‘))) β (πΆ β (Mooreβπ) β§ βπ β π« π(πΉβπ ) = βͺ (πΉ β (π« π β© Fin)))) |