Nearby theorems
|
|
Mathbox for Brendan Leahy |
< Previous
Next >
Nearby theorems |
| Mirrors > Home > MPE Home > Th. List > Mathboxes > poimirlem18 | Structured version Unicode version | |
| Description: Lemma for poimir 31887 stating that, given a face not on a front face of the main cube and a simplex in which it's opposite the first vertex on the walk, there exists exactly one other simplex containing it. (Contributed by Brendan Leahy, 21-Aug-2020.) |
| Ref | Expression |
|---|---|
| poimir.0 |
        |
| poimirlem22.s |
     ..^                       ![]_](_urbrack.gif "]_"){kind=small}      |
| poimirlem22.1 |
|
| poimirlem22.2 |
 |
| poimirlem18.3 |
![/\](wedge.gif "/\"){kind=small}
     |
| poimirlem18.4 |
|
| Ref | Expression |
|---|---|
| poimirlem18 |
  |
,,,,,, ,,, ,,, ,,, ,,, ,, ,,,,, ,,, ,, , ,,,, , ,
,, ,,,,,,() () ()
is distinct from all other
variables.| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | poimir.0 |
. . 3
| |
| 2 | poimirlem22.s |
. . 3
..^ | |
| 3 | poimirlem22.1 |
. . 3
| |
| 4 | poimirlem22.2 |
. . 3
| |
| 5 | poimirlem18.3 |
. . 3
| |
| 6 | poimirlem18.4 |
. . 3
| |
| 7 | 1, 2, 3, 4, 5, 6 | poimirlem17 31871 |
. 2
|
| 8 | 6 | adantr 466 |
. . . . . . . 8
|
| 9 | 0nnn 10642 |
. . . . . . . . . . . . 13
 | |
| 10 | elfznn 11829 |
. . . . . . . . . . . . 13
| |
| 11 | 9, 10 | mto 179 |
. . . . . . . . . . . 12
|
| 12 | eleq1 2494 |
. . . . . . . . . . . 12
| |
| 13 | 11, 12 | mtbiri 304 |
. . . . . . . . . . 11
|
| 14 | 13 | necon2ai 2659 |
. . . . . . . . . 10
|
| 15 | 1 | ad2antrr 730 |
. . . . . . . . . . . . . 14
|
| 16 | fveq2 5878 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 17 | 16 | breq2d 4432 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 18 | 17 | ifbid 3931 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 19 | 18 | csbeq1d 3402 |
. . . . . . . . . . . . . . . . . . . 20
|
| 20 | fveq2 5878 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 21 | 20 | fveq2d 5882 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 22 | 20 | fveq2d 5882 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 23 | 22 | imaeq1d 5183 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 24 | 23 | xpeq1d 4873 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 25 | 22 | imaeq1d 5183 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 26 | 25 | xpeq1d 4873 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 27 | 24, 26 | uneq12d 3621 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 28 | 21, 27 | oveq12d 6320 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 29 | 28 | csbeq2dv 3809 |
. . . . . . . . . . . . . . . . . . . 20
|
| 30 | 19, 29 | eqtrd 2463 |
. . . . . . . . . . . . . . . . . . 19
|
| 31 | 30 | mpteq2dv 4508 |
. . . . . . . . . . . . . . . . . 18
|
| 32 | 31 | eqeq2d 2436 |
. . . . . . . . . . . . . . . . 17
|
| 33 | 32, 2 | elrab2 3231 |
. . . . . . . . . . . . . . . 16
..^
|
| 34 | 33 | simprbi 465 |
. . . . . . . . . . . . . . 15
|
| 35 | 34 | ad2antlr 731 |
. . . . . . . . . . . . . 14
|
| 36 | elrabi 3226 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ | |
| 37 | 36, 2 | eleq2s 2530 |
. . . . . . . . . . . . . . . . . . 19
..^ |
| 38 | xp1st 6834 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ | |
| 39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . 18
..^ |
| 40 | xp1st 6834 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ | |
| 41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^ |
| 42 | elmapi 7498 |
. . . . . . . . . . . . . . . . 17
..^ ..^ | |
| 43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
..^ |
| 44 | elfzoelz 11921 |
. . . . . . . . . . . . . . . . 17
..^
 | |
| 45 | 44 | ssriv 3468 |
. . . . . . . . . . . . . . . 16
..^  |
| 46 | fss 5751 |
. . . . . . . . . . . . . . . 16
..^ ..^
| |
| 47 | 43, 45, 46 | sylancl 666 |
. . . . . . . . . . . . . . 15
|
| 48 | 47 | ad2antlr 731 |
. . . . . . . . . . . . . 14
|
| 49 | xp2nd 6835 |
. . . . . . . . . . . . . . . . 17
..^ | |
| 50 | 39, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
|
| 51 | fvex 5888 |
. . . . . . . . . . . . . . . . 17
 | |
| 52 | f1oeq1 5819 |
. . . . . . . . . . . . . . . . 17
| |
| 53 | 51, 52 | elab 3218 |
. . . . . . . . . . . . . . . 16
|
| 54 | 50, 53 | sylib 199 |
. . . . . . . . . . . . . . 15
|
| 55 | 54 | ad2antlr 731 |
. . . . . . . . . . . . . 14
|
| 56 | simpr 462 |
. . . . . . . . . . . . . 14
| |
| 57 | 15, 35, 48, 55, 56 | poimirlem1 31855 |
. . . . . . . . . . . . 13
|
| 58 | 1 | ad2antrr 730 |
. . . . . . . . . . . . . . . . 17
|
| 59 | fveq2 5878 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 60 | 59 | breq2d 4432 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 61 | 60 | ifbid 3931 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 62 | 61 | csbeq1d 3402 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 63 | fveq2 5878 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 64 | 63 | fveq2d 5882 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 65 | 63 | fveq2d 5882 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 66 | 65 | imaeq1d 5183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 67 | 66 | xpeq1d 4873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 68 | 65 | imaeq1d 5183 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 69 | 68 | xpeq1d 4873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 70 | 67, 69 | uneq12d 3621 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 71 | 64, 70 | oveq12d 6320 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 72 | 71 | csbeq2dv 3809 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 73 | 62, 72 | eqtrd 2463 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 74 | 73 | mpteq2dv 4508 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 75 | 74 | eqeq2d 2436 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 76 | 75, 2 | elrab2 3231 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 77 | 76 | simprbi 465 |
. . . . . . . . . . . . . . . . . . 19
|
| 78 | 4, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
| 79 | 78 | ad2antrr 730 |
. . . . . . . . . . . . . . . . 17
|
| 80 | elrabi 3226 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
..^ | |
| 81 | 80, 2 | eleq2s 2530 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
| 82 | 4, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
| 83 | xp1st 6834 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^ | |
| 84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
| 85 | xp1st 6834 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ | |
| 86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
| 87 | elmapi 7498 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ | |
| 88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
..^ |
| 89 | fss 5751 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
| |
| 90 | 88, 45, 89 | sylancl 666 |
. . . . . . . . . . . . . . . . . 18
|
| 91 | 90 | ad2antrr 730 |
. . . . . . . . . . . . . . . . 17
|
| 92 | xp2nd 6835 |
. . . . . . . . . . . . . . . . . . . 20
..^ | |
| 93 | 84, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
| 94 | fvex 5888 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 95 | f1oeq1 5819 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 96 | 94, 95 | elab 3218 |
. . . . . . . . . . . . . . . . . . 19
|
| 97 | 93, 96 | sylib 199 |
. . . . . . . . . . . . . . . . . 18
|
| 98 | 97 | ad2antrr 730 |
. . . . . . . . . . . . . . . . 17
|
| 99 | simplr 760 |
. . . . . . . . . . . . . . . . 17
| |
| 100 | xp2nd 6835 |
. . . . . . . . . . . . . . . . . . . 20
..^ | |
| 101 | 82, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
| 102 | 101 | adantr 466 |
. . . . . . . . . . . . . . . . . 18
|
| 103 | eldifsn 4122 |
. . . . . . . . . . . . . . . . . . 19
![\](setminus.gif "\"){kind=small}
| |
| 104 | 103 | biimpri 209 |
. . . . . . . . . . . . . . . . . 18
|
| 105 | 102, 104 | sylan 473 |
. . . . . . . . . . . . . . . . 17
|
| 106 | 58, 79, 91, 98, 99, 105 | poimirlem2 31856 |
. . . . . . . . . . . . . . . 16
|
| 107 | 106 | ex 435 |
. . . . . . . . . . . . . . 15
|
| 108 | 107 | necon1bd 2642 |
. . . . . . . . . . . . . 14
|
| 109 | 108 | adantlr 719 |
. . . . . . . . . . . . 13
|
| 110 | 57, 109 | mpd 15 |
. . . . . . . . . . . 12
|
| 111 | 110 | neeq1d 2701 |
. . . . . . . . . . 11
|
| 112 | 111 | exbiri 626 |
. . . . . . . . . 10
|
| 113 | 14, 112 | mpdi 43 |
. . . . . . . . 9
|
| 114 | 113 | necon2bd 2639 |
. . . . . . . 8
|
| 115 | 8, 114 | mpd 15 |
. . . . . . 7
|
| 116 | xp2nd 6835 |
. . . . . . . . 9
..^ | |
| 117 | 37, 116 | syl 17 |
. . . . . . . 8
|
| 118 | 1 | nncnd 10626 |
. . . . . . . . . . . . . . . . . . 19
 |
| 119 | npcan1 10045 |
. . . . . . . . . . . . . . . . . . 19
| |
| 120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
| 121 | nnuz 11195 |
. . . . . . . . . . . . . . . . . . 19
 | |
| 122 | 1, 121 | syl6eleq 2520 |
. . . . . . . . . . . . . . . . . 18
|
| 123 | 120, 122 | eqeltrd 2510 |
. . . . . . . . . . . . . . . . 17
|
| 124 | 1 | nnzd 11040 |
. . . . . . . . . . . . . . . . . . . 20
|
| 125 | peano2zm 10981 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 126 | 124, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
| 127 | uzid 11174 |
. . . . . . . . . . . . . . . . . . 19
| |
| 128 | peano2uz 11213 |
. . . . . . . . . . . . . . . . . . 19
| |
| 129 | 126, 127, 128 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
|
| 130 | 120, 129 | eqeltrrd 2511 |
. . . . . . . . . . . . . . . . 17
|
| 131 | fzsplit2 11825 |
. . . . . . . . . . . . . . . . 17
| |
| 132 | 123, 130, 131 | syl2anc 665 |
. . . . . . . . . . . . . . . 16
|
| 133 | 120 | oveq1d 6317 |
. . . . . . . . . . . . . . . . . 18
|
| 134 | fzsn 11841 |
. . . . . . . . . . . . . . . . . . 19
| |
| 135 | 124, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
| 136 | 133, 135 | eqtrd 2463 |
. . . . . . . . . . . . . . . . 17
|
| 137 | 136 | uneq2d 3620 |
. . . . . . . . . . . . . . . 16
|
| 138 | 132, 137 | eqtrd 2463 |
. . . . . . . . . . . . . . 15
|
| 139 | 138 | eleq2d 2492 |
. . . . . . . . . . . . . 14
|
| 140 | 139 | notbid 295 |
. . . . . . . . . . . . 13
|
| 141 | ioran 492 |
. . . . . . . . . . . . . 14
 | |
| 142 | elun 3606 |
. . . . . . . . . . . . . . 15
| |
| 143 | fvex 5888 |
. . . . . . . . . . . . . . . . 17
| |
| 144 | 143 | elsnc 4020 |
. . . . . . . . . . . . . . . 16
|
| 145 | 144 | orbi2i 521 |
. . . . . . . . . . . . . . 15
|
| 146 | 142, 145 | bitri 252 |
. . . . . . . . . . . . . 14
|
| 147 | 141, 146 | xchnxbir 310 |
. . . . . . . . . . . . 13
|
| 148 | 140, 147 | syl6bb 264 |
. . . . . . . . . . . 12
|
| 149 | 148 | anbi2d 708 |
. . . . . . . . . . 11
|
| 150 | 1 | nnnn0d 10926 |
. . . . . . . . . . . . . . . . 17
 |
| 151 | nn0uz 11194 |
. . . . . . . . . . . . . . . . 17
| |
| 152 | 150, 151 | syl6eleq 2520 |
. . . . . . . . . . . . . . . 16
|
| 153 | fzpred 11845 |
. . . . . . . . . . . . . . . 16
| |
| 154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . . 15
|
| 155 | 154 | difeq1d 3582 |
. . . . . . . . . . . . . 14
|
| 156 | difun2 3875 |
. . . . . . . . . . . . . . 15
| |
| 157 | 0p1e1 10722 |
. . . . . . . . . . . . . . . . . 18
| |
| 158 | 157 | oveq1i 6312 |
. . . . . . . . . . . . . . . . 17
|
| 159 | 158 | uneq2i 3617 |
. . . . . . . . . . . . . . . 16
|
| 160 | 159 | difeq1i 3579 |
. . . . . . . . . . . . . . 15
|
| 161 | incom 3655 |
. . . . . . . . . . . . . . . . 17
 | |
| 162 | elfznn 11829 |
. . . . . . . . . . . . . . . . . . 19
| |
| 163 | 9, 162 | mto 179 |
. . . . . . . . . . . . . . . . . 18
|
| 164 | disjsn 4057 |
. . . . . . . . . . . . . . . . . 18
| |
| 165 | 163, 164 | mpbir 212 |
. . . . . . . . . . . . . . . . 17
|
| 166 | 161, 165 | eqtri 2451 |
. . . . . . . . . . . . . . . 16
|
| 167 | disj3 3837 |
. . . . . . . . . . . . . . . 16
| |
| 168 | 166, 167 | mpbi 211 |
. . . . . . . . . . . . . . 15
|
| 169 | 156, 160, 168 | 3eqtr4i 2461 |
. . . . . . . . . . . . . 14
|
| 170 | 155, 169 | syl6eq 2479 |
. . . . . . . . . . . . 13
|
| 171 | 170 | eleq2d 2492 |
. . . . . . . . . . . 12
|
| 172 | eldif 3446 |
. . . . . . . . . . . 12
| |
| 173 | 143 | elsnc 4020 |
. . . . . . . . . . . 12
|
| 174 | 171, 172, 173 | 3bitr3g 290 |
. . . . . . . . . . 11
|
| 175 | 149, 174 | bitr3d 258 |
. . . . . . . . . 10
|
| 176 | 175 | biimpd 210 |
. . . . . . . . 9
|
| 177 | 176 | expdimp 438 |
. . . . . . . 8
|
| 178 | 117, 177 | sylan2 476 |
. . . . . . 7
|
| 179 | 115, 178 | mpand 679 |
. . . . . 6
|
| 180 | 1, 2, 3 | poimirlem13 31867 |
. . . . . . . . . 10
|
| 181 | fveq2 5878 |
. . . . . . . . . . . 12
| |
| 182 | 181 | eqeq1d 2424 |
. . . . . . . . . . 11
|
| 183 | 182 | rmo4 3264 |
. . . . . . . . . 10
|
| 184 | 180, 183 | sylib 199 |
. . . . . . . . 9
|
| 185 | 184 | r19.21bi 2794 |
. . . . . . . 8
|
| 186 | 4 | adantr 466 |
. . . . . . . 8
|
| 187 | fveq2 5878 |
. . . . . . . . . . . 12
| |
| 188 | 187 | eqeq1d 2424 |
. . . . . . . . . . 11
|
| 189 | 188 | anbi2d 708 |
. . . . . . . . . 10
|
| 190 | eqeq2 2437 |
. . . . . . . . . 10
| |
| 191 | 189, 190 | imbi12d 321 |
. . . . . . . . 9
|
| 192 | 191 | rspccv 3179 |
. . . . . . . 8
|
| 193 | 185, 186, 192 | sylc 62 |
. . . . . . 7
|
| 194 | 8, 193 | mpan2d 678 |
. . . . . 6
|
| 195 | 179, 194 | syld 45 |
. . . . 5
|
| 196 | 195 | necon1ad 2640 |
. . . 4
|
| 197 | 196 | ralrimiva 2839 |
. . 3
|
| 198 | 1, 2, 3 | poimirlem14 31868 |
. . 3
|
| 199 | rmoim 3271 |
. . 3
| |
| 200 | 197, 198, 199 | sylc 62 |
. 2
|
| 201 | reu5 3044 |
. 2
| |
| 202 | 7, 200, 201 | sylanbrc 668 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wo 369
wa 370
wceq 1437
wcel 1868
cab 2407
wne 2618
wral 2775
wrex 2776
wreu 2777
wrmo 2778
crab 2779
csb 3395
cdif 3433
cun 3434
cin 3435
wss 3436
c0 3761
cif 3909
csn 3996
class class class wbr 4420 cmpt 4479 cxp 4848 crn 4851 cima 4853 wf 5594 wf1o 5597
cfv 5598
(class class class)co 6302 cof 6540
c1st 6802
c2nd 6803
cmap 7477
cc 9538
cc0 9540
c1 9541
caddc 9543 clt 9676 cmin 9861 cn 10610 cn0 10870 cz 10938 cuz 11160 cfz 11785 ..^cfzo 11916 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4552 ax-pow 4599 ax-pr 4657 ax-un 6594 ax-cnex 9596 ax-resscn 9597 ax-1cn 9598 ax-icn 9599 ax-addcl 9600 ax-addrcl 9601 ax-mulcl 9602 ax-mulrcl 9603 ax-mulcom 9604 ax-addass 9605 ax-mulass 9606 ax-distr 9607 ax-i2m1 9608 ax-1ne0 9609 ax-1rid 9610 ax-rnegex 9611 ax-rrecex 9612 ax-cnre 9613 ax-pre-lttri 9614 ax-pre-lttrn 9615 ax-pre-ltadd 9616 ax-pre-mulgt0 9617 |
| This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-fal 1443 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-nel 2621 df-ral 2780 df-rex 2781 df-reu 2782 df-rmo 2783 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-tp 4001 df-op 4003 df-uni 4217 df-iun 4298 df-br 4421 df-opab 4480 df-mpt 4481 df-tr 4516 df-eprel 4761 df-id 4765 df-po 4771 df-so 4772 df-fr 4809 df-we 4811 df-xp 4856 df-rel 4857 df-cnv 4858 df-co 4859 df-dm 4860 df-rn 4861 df-res 4862 df-ima 4863 df-pred 5396 df-ord 5442 df-on 5443 df-lim 5444 df-suc 5445 df-iota 5562 df-fun 5600 df-fn 5601 df-f 5602 df-f1 5603 df-fo 5604 df-f1o 5605 df-fv 5606 df-riota 6264 df-ov 6305 df-oprab 6306 df-mpt2 6307 df-of 6542 df-om 6704 df-1st 6804 df-2nd 6805 df-wrecs 7033 df-recs 7095 df-rdg 7133 df-1o 7187 df-er 7368 df-map 7479 df-en 7575 df-dom 7576 df-sdom 7577 df-fin 7578 df-pnf 9678 df-mnf 9679 df-xr 9680 df-ltxr 9681 df-le 9682 df-sub 9863 df-neg 9864 df-nn 10611 df-n0 10871 df-z 10939 df-uz 11161 df-fz 11786 df-fzo 11917 |
| This theorem is referenced by: poimirlem22 31876 |
| Copyright terms: Public domain | W3C validator |