Step | Hyp | Ref
| Expression |
1 | | fvssunirn 6880 |
. . . . 5
β’ (πΉβπ§) β βͺ ran
πΉ |
2 | | simplrr 777 |
. . . . 5
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π¦ β β0 β§ (πΉβπ¦) = βͺ ran πΉ)) β§ π§ β (β€β₯βπ¦)) β (πΉβπ¦) = βͺ ran πΉ) |
3 | 1, 2 | sseqtrrid 4002 |
. . . 4
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π¦ β β0 β§ (πΉβπ¦) = βͺ ran πΉ)) β§ π§ β (β€β₯βπ¦)) β (πΉβπ§) β (πΉβπ¦)) |
4 | | simpll3 1215 |
. . . . 5
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π¦ β β0 β§ (πΉβπ¦) = βͺ ran πΉ)) β§ π§ β (β€β₯βπ¦)) β βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) |
5 | | simplrl 776 |
. . . . 5
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π¦ β β0 β§ (πΉβπ¦) = βͺ ran πΉ)) β§ π§ β (β€β₯βπ¦)) β π¦ β β0) |
6 | | simpr 486 |
. . . . 5
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π¦ β β0 β§ (πΉβπ¦) = βͺ ran πΉ)) β§ π§ β (β€β₯βπ¦)) β π§ β (β€β₯βπ¦)) |
7 | | incssnn0 41063 |
. . . . 5
β’
((βπ₯ β
β0 (πΉβπ₯) β (πΉβ(π₯ + 1)) β§ π¦ β β0 β§ π§ β
(β€β₯βπ¦)) β (πΉβπ¦) β (πΉβπ§)) |
8 | 4, 5, 6, 7 | syl3anc 1372 |
. . . 4
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π¦ β β0 β§ (πΉβπ¦) = βͺ ran πΉ)) β§ π§ β (β€β₯βπ¦)) β (πΉβπ¦) β (πΉβπ§)) |
9 | 3, 8 | eqssd 3966 |
. . 3
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π¦ β β0 β§ (πΉβπ¦) = βͺ ran πΉ)) β§ π§ β (β€β₯βπ¦)) β (πΉβπ§) = (πΉβπ¦)) |
10 | 9 | ralrimiva 3144 |
. 2
β’ (((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π¦ β β0 β§ (πΉβπ¦) = βͺ ran πΉ)) β βπ§ β
(β€β₯βπ¦)(πΉβπ§) = (πΉβπ¦)) |
11 | | frn 6680 |
. . . . . . . 8
β’ (πΉ:β0βΆπΆ β ran πΉ β πΆ) |
12 | 11 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β ran πΉ β πΆ) |
13 | | elpw2g 5306 |
. . . . . . . 8
β’ (πΆ β (NoeACSβπ) β (ran πΉ β π« πΆ β ran πΉ β πΆ)) |
14 | 13 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β (ran πΉ β π« πΆ β ran πΉ β πΆ)) |
15 | 12, 14 | mpbird 257 |
. . . . . 6
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β ran πΉ β π« πΆ) |
16 | | elex 3466 |
. . . . . 6
β’ (ran
πΉ β π« πΆ β ran πΉ β V) |
17 | 15, 16 | syl 17 |
. . . . 5
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β ran πΉ β V) |
18 | | ffn 6673 |
. . . . . . . 8
β’ (πΉ:β0βΆπΆ β πΉ Fn β0) |
19 | 18 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β πΉ Fn β0) |
20 | | 0nn0 12435 |
. . . . . . 7
β’ 0 β
β0 |
21 | | fnfvelrn 7036 |
. . . . . . 7
β’ ((πΉ Fn β0 β§ 0
β β0) β (πΉβ0) β ran πΉ) |
22 | 19, 20, 21 | sylancl 587 |
. . . . . 6
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β (πΉβ0) β ran πΉ) |
23 | 22 | ne0d 4300 |
. . . . 5
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β ran πΉ β β
) |
24 | | nn0re 12429 |
. . . . . . . . 9
β’ (π β β0
β π β
β) |
25 | 24 | ad2antrl 727 |
. . . . . . . 8
β’ (((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β π β
β) |
26 | | nn0re 12429 |
. . . . . . . . 9
β’ (π β β0
β π β
β) |
27 | 26 | ad2antll 728 |
. . . . . . . 8
β’ (((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β π β
β) |
28 | | simplrr 777 |
. . . . . . . . 9
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β π β β0) |
29 | | simpll3 1215 |
. . . . . . . . . . . 12
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) |
30 | | simplrl 776 |
. . . . . . . . . . . 12
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β π β β0) |
31 | | nn0z 12531 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β π β
β€) |
32 | | nn0z 12531 |
. . . . . . . . . . . . . . 15
β’ (π β β0
β π β
β€) |
33 | | eluz 12784 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β€) β (π β
(β€β₯βπ) β π β€ π)) |
34 | 31, 32, 33 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π β
β0) β (π β (β€β₯βπ) β π β€ π)) |
35 | 34 | biimpar 479 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β
β0) β§ π β€ π) β π β (β€β₯βπ)) |
36 | 35 | adantll 713 |
. . . . . . . . . . . 12
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β π β (β€β₯βπ)) |
37 | | incssnn0 41063 |
. . . . . . . . . . . 12
β’
((βπ₯ β
β0 (πΉβπ₯) β (πΉβ(π₯ + 1)) β§ π β β0 β§ π β
(β€β₯βπ)) β (πΉβπ) β (πΉβπ)) |
38 | 29, 30, 36, 37 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β (πΉβπ) β (πΉβπ)) |
39 | | ssequn1 4145 |
. . . . . . . . . . 11
β’ ((πΉβπ) β (πΉβπ) β ((πΉβπ) βͺ (πΉβπ)) = (πΉβπ)) |
40 | 38, 39 | sylib 217 |
. . . . . . . . . 10
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β ((πΉβπ) βͺ (πΉβπ)) = (πΉβπ)) |
41 | | eqimss 4005 |
. . . . . . . . . 10
β’ (((πΉβπ) βͺ (πΉβπ)) = (πΉβπ) β ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
42 | 40, 41 | syl 17 |
. . . . . . . . 9
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
43 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π β (πΉβπ) = (πΉβπ)) |
44 | 43 | sseq2d 3981 |
. . . . . . . . . 10
β’ (π = π β (((πΉβπ) βͺ (πΉβπ)) β (πΉβπ) β ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
45 | 44 | rspcev 3584 |
. . . . . . . . 9
β’ ((π β β0
β§ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) β βπ β β0 ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
46 | 28, 42, 45 | syl2anc 585 |
. . . . . . . 8
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β βπ β β0
((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
47 | | simplrl 776 |
. . . . . . . . 9
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β π β β0) |
48 | | simpll3 1215 |
. . . . . . . . . . . 12
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) |
49 | | simplrr 777 |
. . . . . . . . . . . 12
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β π β β0) |
50 | | eluz 12784 |
. . . . . . . . . . . . . . 15
β’ ((π β β€ β§ π β β€) β (π β
(β€β₯βπ) β π β€ π)) |
51 | 32, 31, 50 | syl2anr 598 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π β
β0) β (π β (β€β₯βπ) β π β€ π)) |
52 | 51 | biimpar 479 |
. . . . . . . . . . . . 13
β’ (((π β β0
β§ π β
β0) β§ π β€ π) β π β (β€β₯βπ)) |
53 | 52 | adantll 713 |
. . . . . . . . . . . 12
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β π β (β€β₯βπ)) |
54 | | incssnn0 41063 |
. . . . . . . . . . . 12
β’
((βπ₯ β
β0 (πΉβπ₯) β (πΉβ(π₯ + 1)) β§ π β β0 β§ π β
(β€β₯βπ)) β (πΉβπ) β (πΉβπ)) |
55 | 48, 49, 53, 54 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β (πΉβπ) β (πΉβπ)) |
56 | | ssequn2 4148 |
. . . . . . . . . . 11
β’ ((πΉβπ) β (πΉβπ) β ((πΉβπ) βͺ (πΉβπ)) = (πΉβπ)) |
57 | 55, 56 | sylib 217 |
. . . . . . . . . 10
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β ((πΉβπ) βͺ (πΉβπ)) = (πΉβπ)) |
58 | | eqimss 4005 |
. . . . . . . . . 10
β’ (((πΉβπ) βͺ (πΉβπ)) = (πΉβπ) β ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
59 | 57, 58 | syl 17 |
. . . . . . . . 9
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
60 | | fveq2 6847 |
. . . . . . . . . . 11
β’ (π = π β (πΉβπ) = (πΉβπ)) |
61 | 60 | sseq2d 3981 |
. . . . . . . . . 10
β’ (π = π β (((πΉβπ) βͺ (πΉβπ)) β (πΉβπ) β ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
62 | 61 | rspcev 3584 |
. . . . . . . . 9
β’ ((π β β0
β§ ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) β βπ β β0 ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
63 | 47, 59, 62 | syl2anc 585 |
. . . . . . . 8
β’ ((((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β§ π β€ π) β βπ β β0
((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
64 | 25, 27, 46, 63 | lecasei 11268 |
. . . . . . 7
β’ (((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β§ (π β β0 β§ π β β0))
β βπ β
β0 ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
65 | 64 | ralrimivva 3198 |
. . . . . 6
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β βπ β β0 βπ β β0
βπ β
β0 ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ)) |
66 | | uneq1 4121 |
. . . . . . . . . . . 12
β’ (π¦ = (πΉβπ) β (π¦ βͺ π§) = ((πΉβπ) βͺ π§)) |
67 | 66 | sseq1d 3980 |
. . . . . . . . . . 11
β’ (π¦ = (πΉβπ) β ((π¦ βͺ π§) β π€ β ((πΉβπ) βͺ π§) β π€)) |
68 | 67 | rexbidv 3176 |
. . . . . . . . . 10
β’ (π¦ = (πΉβπ) β (βπ€ β ran πΉ(π¦ βͺ π§) β π€ β βπ€ β ran πΉ((πΉβπ) βͺ π§) β π€)) |
69 | 68 | ralbidv 3175 |
. . . . . . . . 9
β’ (π¦ = (πΉβπ) β (βπ§ β ran πΉβπ€ β ran πΉ(π¦ βͺ π§) β π€ β βπ§ β ran πΉβπ€ β ran πΉ((πΉβπ) βͺ π§) β π€)) |
70 | 69 | ralrn 7043 |
. . . . . . . 8
β’ (πΉ Fn β0 β
(βπ¦ β ran πΉβπ§ β ran πΉβπ€ β ran πΉ(π¦ βͺ π§) β π€ β βπ β β0 βπ§ β ran πΉβπ€ β ran πΉ((πΉβπ) βͺ π§) β π€)) |
71 | | uneq2 4122 |
. . . . . . . . . . . . 13
β’ (π§ = (πΉβπ) β ((πΉβπ) βͺ π§) = ((πΉβπ) βͺ (πΉβπ))) |
72 | 71 | sseq1d 3980 |
. . . . . . . . . . . 12
β’ (π§ = (πΉβπ) β (((πΉβπ) βͺ π§) β π€ β ((πΉβπ) βͺ (πΉβπ)) β π€)) |
73 | 72 | rexbidv 3176 |
. . . . . . . . . . 11
β’ (π§ = (πΉβπ) β (βπ€ β ran πΉ((πΉβπ) βͺ π§) β π€ β βπ€ β ran πΉ((πΉβπ) βͺ (πΉβπ)) β π€)) |
74 | 73 | ralrn 7043 |
. . . . . . . . . 10
β’ (πΉ Fn β0 β
(βπ§ β ran πΉβπ€ β ran πΉ((πΉβπ) βͺ π§) β π€ β βπ β β0 βπ€ β ran πΉ((πΉβπ) βͺ (πΉβπ)) β π€)) |
75 | | sseq2 3975 |
. . . . . . . . . . . 12
β’ (π€ = (πΉβπ) β (((πΉβπ) βͺ (πΉβπ)) β π€ β ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
76 | 75 | rexrn 7042 |
. . . . . . . . . . 11
β’ (πΉ Fn β0 β
(βπ€ β ran πΉ((πΉβπ) βͺ (πΉβπ)) β π€ β βπ β β0 ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
77 | 76 | ralbidv 3175 |
. . . . . . . . . 10
β’ (πΉ Fn β0 β
(βπ β
β0 βπ€ β ran πΉ((πΉβπ) βͺ (πΉβπ)) β π€ β βπ β β0 βπ β β0
((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
78 | 74, 77 | bitrd 279 |
. . . . . . . . 9
β’ (πΉ Fn β0 β
(βπ§ β ran πΉβπ€ β ran πΉ((πΉβπ) βͺ π§) β π€ β βπ β β0 βπ β β0
((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
79 | 78 | ralbidv 3175 |
. . . . . . . 8
β’ (πΉ Fn β0 β
(βπ β
β0 βπ§ β ran πΉβπ€ β ran πΉ((πΉβπ) βͺ π§) β π€ β βπ β β0 βπ β β0
βπ β
β0 ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
80 | 70, 79 | bitrd 279 |
. . . . . . 7
β’ (πΉ Fn β0 β
(βπ¦ β ran πΉβπ§ β ran πΉβπ€ β ran πΉ(π¦ βͺ π§) β π€ β βπ β β0 βπ β β0
βπ β
β0 ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
81 | 19, 80 | syl 17 |
. . . . . 6
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β (βπ¦ β ran πΉβπ§ β ran πΉβπ€ β ran πΉ(π¦ βͺ π§) β π€ β βπ β β0 βπ β β0
βπ β
β0 ((πΉβπ) βͺ (πΉβπ)) β (πΉβπ))) |
82 | 65, 81 | mpbird 257 |
. . . . 5
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β βπ¦ β ran πΉβπ§ β ran πΉβπ€ β ran πΉ(π¦ βͺ π§) β π€) |
83 | | isipodrs 18433 |
. . . . 5
β’
((toIncβran πΉ)
β Dirset β (ran πΉ
β V β§ ran πΉ β
β
β§ βπ¦
β ran πΉβπ§ β ran πΉβπ€ β ran πΉ(π¦ βͺ π§) β π€)) |
84 | 17, 23, 82, 83 | syl3anbrc 1344 |
. . . 4
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β (toIncβran πΉ) β
Dirset) |
85 | | isnacs3 41062 |
. . . . . . 7
β’ (πΆ β (NoeACSβπ) β (πΆ β (Mooreβπ) β§ βπ¦ β π« πΆ((toIncβπ¦) β Dirset β βͺ π¦
β π¦))) |
86 | 85 | simprbi 498 |
. . . . . 6
β’ (πΆ β (NoeACSβπ) β βπ¦ β π« πΆ((toIncβπ¦) β Dirset β βͺ π¦
β π¦)) |
87 | 86 | 3ad2ant1 1134 |
. . . . 5
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β βπ¦ β π« πΆ((toIncβπ¦) β Dirset β βͺ π¦
β π¦)) |
88 | | fveq2 6847 |
. . . . . . . 8
β’ (π¦ = ran πΉ β (toIncβπ¦) = (toIncβran πΉ)) |
89 | 88 | eleq1d 2823 |
. . . . . . 7
β’ (π¦ = ran πΉ β ((toIncβπ¦) β Dirset β (toIncβran πΉ) β
Dirset)) |
90 | | unieq 4881 |
. . . . . . . 8
β’ (π¦ = ran πΉ β βͺ π¦ = βͺ
ran πΉ) |
91 | | id 22 |
. . . . . . . 8
β’ (π¦ = ran πΉ β π¦ = ran πΉ) |
92 | 90, 91 | eleq12d 2832 |
. . . . . . 7
β’ (π¦ = ran πΉ β (βͺ π¦ β π¦ β βͺ ran
πΉ β ran πΉ)) |
93 | 89, 92 | imbi12d 345 |
. . . . . 6
β’ (π¦ = ran πΉ β (((toIncβπ¦) β Dirset β βͺ π¦
β π¦) β
((toIncβran πΉ) β
Dirset β βͺ ran πΉ β ran πΉ))) |
94 | 93 | rspcva 3582 |
. . . . 5
β’ ((ran
πΉ β π« πΆ β§ βπ¦ β π« πΆ((toIncβπ¦) β Dirset β βͺ π¦
β π¦)) β
((toIncβran πΉ) β
Dirset β βͺ ran πΉ β ran πΉ)) |
95 | 15, 87, 94 | syl2anc 585 |
. . . 4
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β ((toIncβran πΉ) β Dirset β βͺ ran πΉ β ran πΉ)) |
96 | 84, 95 | mpd 15 |
. . 3
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β βͺ
ran πΉ β ran πΉ) |
97 | | fvelrnb 6908 |
. . . 4
β’ (πΉ Fn β0 β
(βͺ ran πΉ β ran πΉ β βπ¦ β β0 (πΉβπ¦) = βͺ ran πΉ)) |
98 | 19, 97 | syl 17 |
. . 3
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β (βͺ
ran πΉ β ran πΉ β βπ¦ β β0
(πΉβπ¦) = βͺ ran πΉ)) |
99 | 96, 98 | mpbid 231 |
. 2
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β βπ¦ β β0 (πΉβπ¦) = βͺ ran πΉ) |
100 | 10, 99 | reximddv 3169 |
1
β’ ((πΆ β (NoeACSβπ) β§ πΉ:β0βΆπΆ β§ βπ₯ β β0
(πΉβπ₯) β (πΉβ(π₯ + 1))) β βπ¦ β β0 βπ§ β
(β€β₯βπ¦)(πΉβπ§) = (πΉβπ¦)) |