Table of ContentsRelated theorems
Unicode version
| Table of Contents |
Mathbox for Jeff Hankins |
< Previous
Next >
Related theorems Unicode version |
| Description: A useful lemma about finite sets. If a property holds for a finite set, it holds for a minimal set. |
| Ref | Expression |
|---|---|
| finminlem.1 |
          |
| Ref | Expression |
|---|---|
| finminlem |
     
|
, , ,| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hbe1 1363 |
. . . . 5
 
| |
| 2 | ax-17 1317 |
. . . . 5
  | |
| 3 | 1, 2 | hbrab 2258 |
. . . 4
 
|
| 4 | ax-17 1317 |
. . . 4
 | |
| 5 | 3, 4 | hbne 2103 |
. . 3
 |
| 6 | isfi 5441 |
. . . 4
| |
| 7 | 19.8a 1376 |
. . . . . . . . . 10
| |
| 8 | 7 | anim2i 362 |
. . . . . . . . 9
|
| 9 | 8 | 3impb 1063 |
. . . . . . . 8
|
| 10 | breq2 3342 |
. . . . . . . . . . 11
| |
| 11 | 10 | anbi1d 679 |
. . . . . . . . . 10
|
| 12 | 11 | exbidv 1657 |
. . . . . . . . 9
|
| 13 | 12 | elrab 2414 |
. . . . . . . 8
|
| 14 | 9, 13 | sylibr 217 |
. . . . . . 7
|
| 15 | ne0i 2881 |
. . . . . . 7
| |
| 16 | 14, 15 | syl 12 |
. . . . . 6
|
| 17 | 16 | 3exp 1066 |
. . . . 5
|
| 18 | 17 | r19.23aiv 2211 |
. . . 4
|
| 19 | 6, 18 | sylbi 216 |
. . 3
|
| 20 | 5, 19 | r19.23ai 2209 |
. 2
|
| 21 | epweon 3864 |
. . 3
   | |
| 22 | ssrab2 2692 |
. . . 4
| |
| 23 | omsson 3954 |
. . . 4
| |
| 24 | 22, 23 | sstri 2626 |
. . 3
|
| 25 | wefrc 3652 |
. . 3
 | |
| 26 | 21, 24, 25 | mp3an12 1181 |
. 2
|
| 27 | ax-17 1317 |
. . . . . . . . 9
| |
| 28 | ax-17 1317 |
. . . . . . . . . . 11
| |
| 29 | 3, 28 | hbin 2800 |
. . . . . . . . . 10
|
| 30 | 29, 4 | hbeq 1995 |
. . . . . . . . 9
|
| 31 | 27, 30 | hban 1356 |
. . . . . . . 8
|
| 32 | simprr 451 |
. . . . . . . . . 10
| |
| 33 | ra4e 2156 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
| |
| 34 | ssfi 5630 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
| |
| 35 | pssss 2705 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 | |
| 36 | 34, 35 | sylan2 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 37 | 36 | ex 402 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 38 | 6, 37 | sylbir 218 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 39 | 33, 38 | syl 12 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 40 | 39 | adantrr 431 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 41 | 40 | adantrr 431 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 42 | simprll 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 43 | simprlr 457 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
| |
| 44 | simplrr 455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
| |
| 45 | visset 2295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
 | |
| 46 | breq1 3341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
| |
| 47 | finminlem.1 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
| |
| 48 | 46, 47 | anbi12d 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 49 | 45, 48 | cla4ev 2371 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 50 | 43, 44, 49 | syl11anc 524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 51 | 33, 6 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
| 52 | 51 | adantrr 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 53 | 52 | adantrr 431 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 54 | 53 | adantr 425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 55 | php3 5609 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 | |
| 56 | 55 | ex 402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 57 | 54, 56 | syl 12 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 58 | endomtr 5479 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
 | |
| 59 | 58 | ex 402 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
| 60 | 59 | ad2antrr 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
| 61 | 60 | ad2antlr 441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 62 | domentr 5480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
| |
| 63 | visset 2295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
| |
| 64 | 63 | ensym 5471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
|
| 65 | 62, 64 | sylan2 500 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
|
| 66 | 65 | expcom 403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
|
| 67 | 66 | ad2antll 443 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
|
| 68 | 61, 67 | syld 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 69 | visset 2295 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
| |
| 70 | ssdomg 5467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
| |
| 71 | 69, 70 | ax-mp 7 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
|
| 72 | 68, 71 | syl5 20 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 73 | domnsym 5526 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
 | |
| 74 | 73 | con2i 113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
|
| 75 | 72, 74 | nsyli 136 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 76 | 57, 75 | syld 30 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 77 | 76 | impr 422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 78 | nnord 3959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
 | |
| 79 | 78 | ad2antrr 440 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 80 | nnord 3959 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
| |
| 81 | 80 | adantr 425 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 82 | 81 | ad2antrl 442 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 83 | ordtri1 3693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
| |
| 84 | 83 | con2bid 585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 85 | 79, 82, 84 | syl11anc 524 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 86 | 77, 85 | mpbird 213 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 87 | 42, 50, 86 | jca31 311 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 88 | elin 2786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
| |
| 89 | breq2 3342 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
| |
| 90 | 89 | anbi1d 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
|
| 91 | 90 | exbidv 1657 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
|
| 92 | 91 | elrab 2414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
|
| 93 | 92 | anbi1i 539 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
| 94 | 88, 93 | bitri 190 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
| 95 | 87, 94 | sylibr 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
| 96 | ne0i 2881 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
| |
| 97 | 95, 96 | syl 12 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
| 98 | 97 | exp44 416 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
| 99 | 98 | r19.23adv 2215 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
| 100 | isfi 5441 |
. . . . . . . . . . . . . . . . . . . . . . . 24
| |
| 101 | 99, 100 | syl5ib 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
| 102 | 101 | com23 36 |
. . . . . . . . . . . . . . . . . . . . . 22
|
| 103 | 41, 102 | mpdd 57 |
. . . . . . . . . . . . . . . . . . . . 21
|
| 104 | 103 | necon2bd 2057 |
. . . . . . . . . . . . . . . . . . . 20
|
| 105 | 104 | ex 402 |
. . . . . . . . . . . . . . . . . . 19
|
| 106 | 105 | com23 36 |
. . . . . . . . . . . . . . . . . 18
|
| 107 | 106 | imp31 389 |
. . . . . . . . . . . . . . . . 17
|
| 108 | 107 | pm2.21d 94 |
. . . . . . . . . . . . . . . 16
|
| 109 | eqcom 1886 |
. . . . . . . . . . . . . . . . . 18
| |
| 110 | 109 | biimpi 168 |
. . . . . . . . . . . . . . . . 17
|
| 111 | 110 | a1i 8 |
. . . . . . . . . . . . . . . 16
|
| 112 | 108, 111 | jaod 469 |
. . . . . . . . . . . . . . 15
 |
| 113 | sspss 2707 |
. . . . . . . . . . . . . . 15
| |
| 114 | 112, 113 | syl5ib 223 |
. . . . . . . . . . . . . 14
|
| 115 | 114 | expr 418 |
. . . . . . . . . . . . 13
|
| 116 | 115 | com23 36 |
. . . . . . . . . . . 12
|
| 117 | 116 | imp3a 388 |
. . . . . . . . . . 11
|
| 118 | 117 | 19.21aiv 1664 |
. . . . . . . . . 10
|
| 119 | 32, 118 | jca 310 |
. . . . . . . . 9
|
| 120 | 119 | ex 402 |
. . . . . . . 8
|
| 121 | 31, 120 | eximd 1410 |
. . . . . . 7
|
| 122 | 121 | ex 402 |
. . . . . 6
|
| 123 | 122 | com23 36 |
. . . . 5
|
| 124 | 123 | imp 377 |
. . . 4
|
| 125 | 13, 124 | sylbi 216 |
. . 3
|
| 126 | 125 | r19.23aiv 2211 |
. 2
|
| 127 | 20, 26, 126 | 3syl 24 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wn 2
wi 3
wb 163
wo 239
wa 240
w3a 858
wal 1296
wceq 1298
wcel 1300
wex 1326
wne 2017
wrex 2106
crab 2108
cvv 2292
cin 2592
wss 2593
wpss 2594
c0 2875
class class class wbr 3338 cep 3581 wwe 3624 word 3656 con0 3657 com 3949 cen 5423 cdom 5424 csdm 5425 cfn 5426 |
| This theorem is referenced by: filfinnfr 15561 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-rab 2112 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-f 4010 df-f1 4011 df-fo 4012 df-f1o 4013 df-fv 4014 df-er 5318 df-en 5427 df-dom 5428 df-sdom 5429 df-fin 5430 |