Step | Hyp | Ref
| Expression |
1 | | fvssunirn 6217 |
. . . . 5
|
2 | | simplrr 801 |
. . . . 5
NoeACS
|
3 | 1, 2 | syl5sseqr 3654 |
. . . 4
NoeACS
|
4 | | simpll3 1102 |
. . . . 5
NoeACS
|
5 | | simplrl 800 |
. . . . 5
NoeACS
|
6 | | simpr 477 |
. . . . 5
NoeACS
|
7 | | incssnn0 37274 |
. . . . 5
|
8 | 4, 5, 6, 7 | syl3anc 1326 |
. . . 4
NoeACS
|
9 | 3, 8 | eqssd 3620 |
. . 3
NoeACS
|
10 | 9 | ralrimiva 2966 |
. 2
NoeACS
|
11 | | frn 6053 |
. . . . . . . 8
|
12 | 11 | 3ad2ant2 1083 |
. . . . . . 7
NoeACS
|
13 | | elpw2g 4827 |
. . . . . . . 8
NoeACS
|
14 | 13 | 3ad2ant1 1082 |
. . . . . . 7
NoeACS
|
15 | 12, 14 | mpbird 247 |
. . . . . 6
NoeACS
|
16 | | elex 3212 |
. . . . . 6
|
17 | 15, 16 | syl 17 |
. . . . 5
NoeACS
|
18 | | ffn 6045 |
. . . . . . . 8
|
19 | 18 | 3ad2ant2 1083 |
. . . . . . 7
NoeACS
|
20 | | 0nn0 11307 |
. . . . . . 7
|
21 | | fnfvelrn 6356 |
. . . . . . 7
|
22 | 19, 20, 21 | sylancl 694 |
. . . . . 6
NoeACS
|
23 | | ne0i 3921 |
. . . . . 6
|
24 | 22, 23 | syl 17 |
. . . . 5
NoeACS
|
25 | | nn0re 11301 |
. . . . . . . . 9
|
26 | 25 | ad2antrl 764 |
. . . . . . . 8
NoeACS
|
27 | | nn0re 11301 |
. . . . . . . . 9
|
28 | 27 | ad2antll 765 |
. . . . . . . 8
NoeACS
|
29 | | simplrr 801 |
. . . . . . . . 9
NoeACS
|
30 | | simpll3 1102 |
. . . . . . . . . . . 12
NoeACS
|
31 | | simplrl 800 |
. . . . . . . . . . . 12
NoeACS
|
32 | | nn0z 11400 |
. . . . . . . . . . . . . . 15
|
33 | | nn0z 11400 |
. . . . . . . . . . . . . . 15
|
34 | | eluz 11701 |
. . . . . . . . . . . . . . 15
|
35 | 32, 33, 34 | syl2an 494 |
. . . . . . . . . . . . . 14
|
36 | 35 | biimpar 502 |
. . . . . . . . . . . . 13
|
37 | 36 | adantll 750 |
. . . . . . . . . . . 12
NoeACS
|
38 | | incssnn0 37274 |
. . . . . . . . . . . 12
|
39 | 30, 31, 37, 38 | syl3anc 1326 |
. . . . . . . . . . 11
NoeACS
|
40 | | ssequn1 3783 |
. . . . . . . . . . 11
|
41 | 39, 40 | sylib 208 |
. . . . . . . . . 10
NoeACS
|
42 | | eqimss 3657 |
. . . . . . . . . 10
|
43 | 41, 42 | syl 17 |
. . . . . . . . 9
NoeACS
|
44 | | fveq2 6191 |
. . . . . . . . . . 11
|
45 | 44 | sseq2d 3633 |
. . . . . . . . . 10
|
46 | 45 | rspcev 3309 |
. . . . . . . . 9
|
47 | 29, 43, 46 | syl2anc 693 |
. . . . . . . 8
NoeACS
|
48 | | simplrl 800 |
. . . . . . . . 9
NoeACS
|
49 | | simpll3 1102 |
. . . . . . . . . . . 12
NoeACS
|
50 | | simplrr 801 |
. . . . . . . . . . . 12
NoeACS
|
51 | | eluz 11701 |
. . . . . . . . . . . . . . 15
|
52 | 33, 32, 51 | syl2anr 495 |
. . . . . . . . . . . . . 14
|
53 | 52 | biimpar 502 |
. . . . . . . . . . . . 13
|
54 | 53 | adantll 750 |
. . . . . . . . . . . 12
NoeACS
|
55 | | incssnn0 37274 |
. . . . . . . . . . . 12
|
56 | 49, 50, 54, 55 | syl3anc 1326 |
. . . . . . . . . . 11
NoeACS
|
57 | | ssequn2 3786 |
. . . . . . . . . . 11
|
58 | 56, 57 | sylib 208 |
. . . . . . . . . 10
NoeACS
|
59 | | eqimss 3657 |
. . . . . . . . . 10
|
60 | 58, 59 | syl 17 |
. . . . . . . . 9
NoeACS
|
61 | | fveq2 6191 |
. . . . . . . . . . 11
|
62 | 61 | sseq2d 3633 |
. . . . . . . . . 10
|
63 | 62 | rspcev 3309 |
. . . . . . . . 9
|
64 | 48, 60, 63 | syl2anc 693 |
. . . . . . . 8
NoeACS
|
65 | 26, 28, 47, 64 | lecasei 10143 |
. . . . . . 7
NoeACS
|
66 | 65 | ralrimivva 2971 |
. . . . . 6
NoeACS
|
67 | | uneq1 3760 |
. . . . . . . . . . . 12
|
68 | 67 | sseq1d 3632 |
. . . . . . . . . . 11
|
69 | 68 | rexbidv 3052 |
. . . . . . . . . 10
|
70 | 69 | ralbidv 2986 |
. . . . . . . . 9
|
71 | 70 | ralrn 6362 |
. . . . . . . 8
|
72 | | uneq2 3761 |
. . . . . . . . . . . . 13
|
73 | 72 | sseq1d 3632 |
. . . . . . . . . . . 12
|
74 | 73 | rexbidv 3052 |
. . . . . . . . . . 11
|
75 | 74 | ralrn 6362 |
. . . . . . . . . 10
|
76 | | sseq2 3627 |
. . . . . . . . . . . 12
|
77 | 76 | rexrn 6361 |
. . . . . . . . . . 11
|
78 | 77 | ralbidv 2986 |
. . . . . . . . . 10
|
79 | 75, 78 | bitrd 268 |
. . . . . . . . 9
|
80 | 79 | ralbidv 2986 |
. . . . . . . 8
|
81 | 71, 80 | bitrd 268 |
. . . . . . 7
|
82 | 19, 81 | syl 17 |
. . . . . 6
NoeACS
|
83 | 66, 82 | mpbird 247 |
. . . . 5
NoeACS
|
84 | | isipodrs 17161 |
. . . . 5
toInc Dirset
|
85 | 17, 24, 83, 84 | syl3anbrc 1246 |
. . . 4
NoeACS
toInc
Dirset |
86 | | isnacs3 37273 |
. . . . . . 7
NoeACS Moore toInc Dirset |
87 | 86 | simprbi 480 |
. . . . . 6
NoeACS
toInc Dirset |
88 | 87 | 3ad2ant1 1082 |
. . . . 5
NoeACS
toInc Dirset |
89 | | fveq2 6191 |
. . . . . . . 8
toInc toInc |
90 | 89 | eleq1d 2686 |
. . . . . . 7
toInc Dirset
toInc Dirset |
91 | | unieq 4444 |
. . . . . . . 8
|
92 | | id 22 |
. . . . . . . 8
|
93 | 91, 92 | eleq12d 2695 |
. . . . . . 7
|
94 | 90, 93 | imbi12d 334 |
. . . . . 6
toInc Dirset toInc Dirset
|
95 | 94 | rspcva 3307 |
. . . . 5
toInc Dirset
toInc Dirset |
96 | 15, 88, 95 | syl2anc 693 |
. . . 4
NoeACS
toInc Dirset |
97 | 85, 96 | mpd 15 |
. . 3
NoeACS
|
98 | | fvelrnb 6243 |
. . . 4
|
99 | 19, 98 | syl 17 |
. . 3
NoeACS
|
100 | 97, 99 | mpbid 222 |
. 2
NoeACS
|
101 | 10, 100 | reximddv 3018 |
1
NoeACS
|