Nearby theorems
|
|
Mathbox for Brendan Leahy |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > poimirlem18 | Structured version Visualization version Unicode version | ||
| Description: Lemma for poimir 32037 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 32021 |
. 2
|
| 8 | 6 | adantr 472 |
. . . . . . . 8
|
| 9 | 0nnn 10663 |
. . . . . . . . . . . . 13
 | |
| 10 | elfznn 11854 |
. . . . . . . . . . . . 13
| |
| 11 | 9, 10 | mto 181 |
. . . . . . . . . . . 12
|
| 12 | eleq1 2537 |
. . . . . . . . . . . 12
| |
| 13 | 11, 12 | mtbiri 310 |
. . . . . . . . . . 11
|
| 14 | 13 | necon2ai 2672 |
. . . . . . . . . 10
|
| 15 | 1 | ad2antrr 740 |
. . . . . . . . . . . . . 14
|
| 16 | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 17 | 16 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 18 | 17 | ifbid 3894 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 19 | 18 | csbeq1d 3356 |
. . . . . . . . . . . . . . . . . . . 20
|
| 20 | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . 23
| |
| 21 | 20 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 22 | 20 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 23 | 22 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 24 | 23 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 25 | 22 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 26 | 25 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 27 | 24, 26 | uneq12d 3580 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 28 | 21, 27 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 29 | 28 | csbeq2dv 3785 |
. . . . . . . . . . . . . . . . . . . 20
|
| 30 | 19, 29 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . 19
|
| 31 | 30 | mpteq2dv 4483 |
. . . . . . . . . . . . . . . . . 18
|
| 32 | 31 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . 17
|
| 33 | 32, 2 | elrab2 3186 |
. . . . . . . . . . . . . . . 16
..^
|
| 34 | 33 | simprbi 471 |
. . . . . . . . . . . . . . 15
|
| 35 | 34 | ad2antlr 741 |
. . . . . . . . . . . . . 14
|
| 36 | elrabi 3181 |
. . . . . . . . . . . . . . . . . . . 20
..^
..^ | |
| 37 | 36, 2 | eleq2s 2567 |
. . . . . . . . . . . . . . . . . . 19
..^ |
| 38 | xp1st 6842 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^ | |
| 39 | 37, 38 | syl 17 |
. . . . . . . . . . . . . . . . . 18
..^ |
| 40 | xp1st 6842 |
. . . . . . . . . . . . . . . . . 18
..^ ..^ | |
| 41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . . . . 17
..^ |
| 42 | elmapi 7511 |
. . . . . . . . . . . . . . . . 17
..^ ..^ | |
| 43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
..^ |
| 44 | elfzoelz 11947 |
. . . . . . . . . . . . . . . . 17
..^
 | |
| 45 | 44 | ssriv 3422 |
. . . . . . . . . . . . . . . 16
..^  |
| 46 | fss 5749 |
. . . . . . . . . . . . . . . 16
..^ ..^
| |
| 47 | 43, 45, 46 | sylancl 675 |
. . . . . . . . . . . . . . 15
|
| 48 | 47 | ad2antlr 741 |
. . . . . . . . . . . . . 14
|
| 49 | xp2nd 6843 |
. . . . . . . . . . . . . . . . 17
..^ | |
| 50 | 39, 49 | syl 17 |
. . . . . . . . . . . . . . . 16
|
| 51 | fvex 5889 |
. . . . . . . . . . . . . . . . 17
 | |
| 52 | f1oeq1 5818 |
. . . . . . . . . . . . . . . . 17
| |
| 53 | 51, 52 | elab 3173 |
. . . . . . . . . . . . . . . 16
|
| 54 | 50, 53 | sylib 201 |
. . . . . . . . . . . . . . 15
|
| 55 | 54 | ad2antlr 741 |
. . . . . . . . . . . . . 14
|
| 56 | simpr 468 |
. . . . . . . . . . . . . 14
| |
| 57 | 15, 35, 48, 55, 56 | poimirlem1 32005 |
. . . . . . . . . . . . 13
|
| 58 | 1 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
|
| 59 | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 60 | 59 | breq2d 4407 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 61 | 60 | ifbid 3894 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 62 | 61 | csbeq1d 3356 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 63 | fveq2 5879 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 64 | 63 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 65 | 63 | fveq2d 5883 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 66 | 65 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 67 | 66 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 68 | 65 | imaeq1d 5173 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 69 | 68 | xpeq1d 4862 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 70 | 67, 69 | uneq12d 3580 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 71 | 64, 70 | oveq12d 6326 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 72 | 71 | csbeq2dv 3785 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 73 | 62, 72 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 74 | 73 | mpteq2dv 4483 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 75 | 74 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 76 | 75, 2 | elrab2 3186 |
. . . . . . . . . . . . . . . . . . . 20
..^
|
| 77 | 76 | simprbi 471 |
. . . . . . . . . . . . . . . . . . 19
|
| 78 | 4, 77 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
| 79 | 78 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
|
| 80 | elrabi 3181 |
. . . . . . . . . . . . . . . . . . . . . . . 24
..^
..^ | |
| 81 | 80, 2 | eleq2s 2567 |
. . . . . . . . . . . . . . . . . . . . . . 23
..^ |
| 82 | 4, 81 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ |
| 83 | xp1st 6842 |
. . . . . . . . . . . . . . . . . . . . . 22
..^ ..^ | |
| 84 | 82, 83 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
..^ |
| 85 | xp1st 6842 |
. . . . . . . . . . . . . . . . . . . . 21
..^ ..^ | |
| 86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
..^ |
| 87 | elmapi 7511 |
. . . . . . . . . . . . . . . . . . . 20
..^ ..^ | |
| 88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
..^ |
| 89 | fss 5749 |
. . . . . . . . . . . . . . . . . . 19
..^ ..^
| |
| 90 | 88, 45, 89 | sylancl 675 |
. . . . . . . . . . . . . . . . . 18
|
| 91 | 90 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
|
| 92 | xp2nd 6843 |
. . . . . . . . . . . . . . . . . . . 20
..^ | |
| 93 | 84, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
| 94 | fvex 5889 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 95 | f1oeq1 5818 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 96 | 94, 95 | elab 3173 |
. . . . . . . . . . . . . . . . . . 19
|
| 97 | 93, 96 | sylib 201 |
. . . . . . . . . . . . . . . . . 18
|
| 98 | 97 | ad2antrr 740 |
. . . . . . . . . . . . . . . . 17
|
| 99 | simplr 770 |
. . . . . . . . . . . . . . . . 17
| |
| 100 | xp2nd 6843 |
. . . . . . . . . . . . . . . . . . . 20
..^ | |
| 101 | 82, 100 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
| 102 | 101 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
|
| 103 | eldifsn 4088 |
. . . . . . . . . . . . . . . . . . 19
![\](setminus.gif "\"){kind=small}
| |
| 104 | 103 | biimpri 211 |
. . . . . . . . . . . . . . . . . 18
|
| 105 | 102, 104 | sylan 479 |
. . . . . . . . . . . . . . . . 17
|
| 106 | 58, 79, 91, 98, 99, 105 | poimirlem2 32006 |
. . . . . . . . . . . . . . . 16
|
| 107 | 106 | ex 441 |
. . . . . . . . . . . . . . 15
|
| 108 | 107 | necon1bd 2661 |
. . . . . . . . . . . . . 14
|
| 109 | 108 | adantlr 729 |
. . . . . . . . . . . . 13
|
| 110 | 57, 109 | mpd 15 |
. . . . . . . . . . . 12
|
| 111 | 110 | neeq1d 2702 |
. . . . . . . . . . 11
|
| 112 | 111 | exbiri 634 |
. . . . . . . . . 10
|
| 113 | 14, 112 | mpdi 42 |
. . . . . . . . 9
|
| 114 | 113 | necon2bd 2659 |
. . . . . . . 8
|
| 115 | 8, 114 | mpd 15 |
. . . . . . 7
|
| 116 | xp2nd 6843 |
. . . . . . . . 9
..^ | |
| 117 | 37, 116 | syl 17 |
. . . . . . . 8
|
| 118 | 1 | nncnd 10647 |
. . . . . . . . . . . . . . . . . . 19
 |
| 119 | npcan1 10065 |
. . . . . . . . . . . . . . . . . . 19
| |
| 120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
| 121 | nnuz 11218 |
. . . . . . . . . . . . . . . . . . 19
 | |
| 122 | 1, 121 | syl6eleq 2559 |
. . . . . . . . . . . . . . . . . 18
|
| 123 | 120, 122 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . 17
|
| 124 | 1 | nnzd 11062 |
. . . . . . . . . . . . . . . . . . . 20
|
| 125 | peano2zm 11004 |
. . . . . . . . . . . . . . . . . . . 20
| |
| 126 | 124, 125 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
|
| 127 | uzid 11197 |
. . . . . . . . . . . . . . . . . . 19
| |
| 128 | peano2uz 11235 |
. . . . . . . . . . . . . . . . . . 19
| |
| 129 | 126, 127, 128 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
|
| 130 | 120, 129 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . 17
|
| 131 | fzsplit2 11850 |
. . . . . . . . . . . . . . . . 17
| |
| 132 | 123, 130, 131 | syl2anc 673 |
. . . . . . . . . . . . . . . 16
|
| 133 | 120 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
|
| 134 | fzsn 11866 |
. . . . . . . . . . . . . . . . . . 19
| |
| 135 | 124, 134 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
| 136 | 133, 135 | eqtrd 2505 |
. . . . . . . . . . . . . . . . 17
|
| 137 | 136 | uneq2d 3579 |
. . . . . . . . . . . . . . . 16
|
| 138 | 132, 137 | eqtrd 2505 |
. . . . . . . . . . . . . . 15
|
| 139 | 138 | eleq2d 2534 |
. . . . . . . . . . . . . 14
|
| 140 | 139 | notbid 301 |
. . . . . . . . . . . . 13
|
| 141 | ioran 498 |
. . . . . . . . . . . . . 14
 | |
| 142 | elun 3565 |
. . . . . . . . . . . . . . 15
| |
| 143 | fvex 5889 |
. . . . . . . . . . . . . . . . 17
| |
| 144 | 143 | elsnc 3984 |
. . . . . . . . . . . . . . . 16
|
| 145 | 144 | orbi2i 528 |
. . . . . . . . . . . . . . 15
|
| 146 | 142, 145 | bitri 257 |
. . . . . . . . . . . . . 14
|
| 147 | 141, 146 | xchnxbir 316 |
. . . . . . . . . . . . 13
|
| 148 | 140, 147 | syl6bb 269 |
. . . . . . . . . . . 12
|
| 149 | 148 | anbi2d 718 |
. . . . . . . . . . 11
|
| 150 | 1 | nnnn0d 10949 |
. . . . . . . . . . . . . . . . 17
 |
| 151 | nn0uz 11217 |
. . . . . . . . . . . . . . . . 17
| |
| 152 | 150, 151 | syl6eleq 2559 |
. . . . . . . . . . . . . . . 16
|
| 153 | fzpred 11870 |
. . . . . . . . . . . . . . . 16
| |
| 154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . . 15
|
| 155 | 154 | difeq1d 3539 |
. . . . . . . . . . . . . 14
|
| 156 | difun2 3838 |
. . . . . . . . . . . . . . 15
| |
| 157 | 0p1e1 10743 |
. . . . . . . . . . . . . . . . . 18
| |
| 158 | 157 | oveq1i 6318 |
. . . . . . . . . . . . . . . . 17
|
| 159 | 158 | uneq2i 3576 |
. . . . . . . . . . . . . . . 16
|
| 160 | 159 | difeq1i 3536 |
. . . . . . . . . . . . . . 15
|
| 161 | incom 3616 |
. . . . . . . . . . . . . . . . 17
 | |
| 162 | elfznn 11854 |
. . . . . . . . . . . . . . . . . . 19
| |
| 163 | 9, 162 | mto 181 |
. . . . . . . . . . . . . . . . . 18
|
| 164 | disjsn 4023 |
. . . . . . . . . . . . . . . . . 18
| |
| 165 | 163, 164 | mpbir 214 |
. . . . . . . . . . . . . . . . 17
|
| 166 | 161, 165 | eqtri 2493 |
. . . . . . . . . . . . . . . 16
|
| 167 | disj3 3813 |
. . . . . . . . . . . . . . . 16
| |
| 168 | 166, 167 | mpbi 213 |
. . . . . . . . . . . . . . 15
|
| 169 | 156, 160, 168 | 3eqtr4i 2503 |
. . . . . . . . . . . . . 14
|
| 170 | 155, 169 | syl6eq 2521 |
. . . . . . . . . . . . 13
|
| 171 | 170 | eleq2d 2534 |
. . . . . . . . . . . 12
|
| 172 | eldif 3400 |
. . . . . . . . . . . 12
| |
| 173 | 143 | elsnc 3984 |
. . . . . . . . . . . 12
|
| 174 | 171, 172, 173 | 3bitr3g 295 |
. . . . . . . . . . 11
|
| 175 | 149, 174 | bitr3d 263 |
. . . . . . . . . 10
|
| 176 | 175 | biimpd 212 |
. . . . . . . . 9
|
| 177 | 176 | expdimp 444 |
. . . . . . . 8
|
| 178 | 117, 177 | sylan2 482 |
. . . . . . 7
|
| 179 | 115, 178 | mpand 689 |
. . . . . 6
|
| 180 | 1, 2, 3 | poimirlem13 32017 |
. . . . . . . . . 10
|
| 181 | fveq2 5879 |
. . . . . . . . . . . 12
| |
| 182 | 181 | eqeq1d 2473 |
. . . . . . . . . . 11
|
| 183 | 182 | rmo4 3219 |
. . . . . . . . . 10
|
| 184 | 180, 183 | sylib 201 |
. . . . . . . . 9
|
| 185 | 184 | r19.21bi 2776 |
. . . . . . . 8
|
| 186 | 4 | adantr 472 |
. . . . . . . 8
|
| 187 | fveq2 5879 |
. . . . . . . . . . . 12
| |
| 188 | 187 | eqeq1d 2473 |
. . . . . . . . . . 11
|
| 189 | 188 | anbi2d 718 |
. . . . . . . . . 10
|
| 190 | eqeq2 2482 |
. . . . . . . . . 10
| |
| 191 | 189, 190 | imbi12d 327 |
. . . . . . . . 9
|
| 192 | 191 | rspccv 3133 |
. . . . . . . 8
|
| 193 | 185, 186, 192 | sylc 61 |
. . . . . . 7
|
| 194 | 8, 193 | mpan2d 688 |
. . . . . 6
|
| 195 | 179, 194 | syld 44 |
. . . . 5
|
| 196 | 195 | necon1ad 2660 |
. . . 4
|
| 197 | 196 | ralrimiva 2809 |
. . 3
|
| 198 | 1, 2, 3 | poimirlem14 32018 |
. . 3
|
| 199 | rmoim 3227 |
. . 3
| |
| 200 | 197, 198, 199 | sylc 61 |
. 2
|
| 201 | reu5 2994 |
. 2
| |
| 202 | 7, 200, 201 | sylanbrc 677 |
1
|
| Colors of variables: wff setvar class |
| Syntax hints: wn 3
wi 4
wo 375
wa 376
wceq 1452
wcel 1904
cab 2457
wne 2641
wral 2756
wrex 2757
wreu 2758
wrmo 2759
crab 2760
csb 3349
cdif 3387
cun 3388
cin 3389
wss 3390
c0 3722
cif 3872
csn 3959
class class class wbr 4395 cmpt 4454 cxp 4837 crn 4840 cima 4842 wf 5585 wf1o 5588
cfv 5589
(class class class)co 6308 cof 6548
c1st 6810
c2nd 6811
cmap 7490
cc 9555
cc0 9557
c1 9558
caddc 9560 clt 9693 cmin 9880 cn 10631 cn0 10893 cz 10961 cuz 11182 cfz 11810 ..^cfzo 11942 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-cnex 9613 ax-resscn 9614 ax-1cn 9615 ax-icn 9616 ax-addcl 9617 ax-addrcl 9618 ax-mulcl 9619 ax-mulrcl 9620 ax-mulcom 9621 ax-addass 9622 ax-mulass 9623 ax-distr 9624 ax-i2m1 9625 ax-1ne0 9626 ax-1rid 9627 ax-rnegex 9628 ax-rrecex 9629 ax-cnre 9630 ax-pre-lttri 9631 ax-pre-lttrn 9632 ax-pre-ltadd 9633 ax-pre-mulgt0 9634 |
| This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-fal 1458 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-iun 4271 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-of 6550 df-om 6712 df-1st 6812 df-2nd 6813 df-wrecs 7046 df-recs 7108 df-rdg 7146 df-1o 7200 df-er 7381 df-map 7492 df-en 7588 df-dom 7589 df-sdom 7590 df-fin 7591 df-pnf 9695 df-mnf 9696 df-xr 9697 df-ltxr 9698 df-le 9699 df-sub 9882 df-neg 9883 df-nn 10632 df-n0 10894 df-z 10962 df-uz 11183 df-fz 11811 df-fzo 11943 |
| This theorem is referenced by: poimirlem22 32026 |
| Copyright terms: Public domain | W3C validator |