Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  noinfep Unicode version

Theorem noinfep 7362
 Description: Using the Axiom of Regularity in the form zfregfr 7318, show that there are no infinite descending -chains. Proposition 7.34 of [TakeutiZaring] p. 44. (Contributed by NM, 26-Jan-2006.) (Revised by Mario Carneiro, 22-Mar-2013.)
Assertion
Ref Expression
noinfep
Distinct variable group:   ,

Proof of Theorem noinfep
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omex 7346 . . . . 5
21mptex 5748 . . . 4
32rnex 4944 . . 3
4 zfregfr 7318 . . 3
5 ssid 3199 . . 3
6 dmmptg 5172 . . . . . 6
7 fvex 5541 . . . . . . 7
87a1i 10 . . . . . 6
96, 8mprg 2614 . . . . 5
10 peano1 4677 . . . . . 6
11 ne0i 3463 . . . . . 6
1210, 11ax-mp 8 . . . . 5
139, 12eqnetri 2465 . . . 4
14 dm0rn0 4897 . . . . 5
1514necon3bii 2480 . . . 4
1613, 15mpbi 199 . . 3
17 fri 4357 . . 3
183, 4, 5, 16, 17mp4an 654 . 2
19 eqid 2285 . . . . . . 7
207, 19fnmpti 5374 . . . . . 6
21 fvelrnb 5572 . . . . . 6
2220, 21ax-mp 8 . . . . 5
23 peano2 4678 . . . . . . . . . . 11
24 fveq2 5527 . . . . . . . . . . . 12
25 fvex 5541 . . . . . . . . . . . 12
2624, 19, 25fvmpt 5604 . . . . . . . . . . 11
2723, 26syl 15 . . . . . . . . . 10
28 fnfvelrn 5664 . . . . . . . . . . 11
2920, 23, 28sylancr 644 . . . . . . . . . 10
3027, 29eqeltrrd 2360 . . . . . . . . 9
31 epel 4310 . . . . . . . . . . . . 13
32 eleq1 2345 . . . . . . . . . . . . 13
3331, 32syl5bb 248 . . . . . . . . . . . 12
3433notbid 285 . . . . . . . . . . 11
35 df-nel 2451 . . . . . . . . . . 11
3634, 35syl6bbr 254 . . . . . . . . . 10
3736rspccv 2883 . . . . . . . . 9
3830, 37syl5com 26 . . . . . . . 8
39 fveq2 5527 . . . . . . . . . . . 12
40 fvex 5541 . . . . . . . . . . . 12
4139, 19, 40fvmpt 5604 . . . . . . . . . . 11
42 eqeq1 2291 . . . . . . . . . . 11
4341, 42syl5ibcom 211 . . . . . . . . . 10
44 neleq2 2540 . . . . . . . . . . 11
4544biimpd 198 . . . . . . . . . 10
4643, 45syl6 29 . . . . . . . . 9
4746com23 72 . . . . . . . 8
4838, 47syld 40 . . . . . . 7
4948com12 27 . . . . . 6
5049reximdvai 2655 . . . . 5
5122, 50syl5bi 208 . . . 4
5251com12 27 . . 3
5352rexlimiv 2663 . 2
5418, 53ax-mp 8 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wceq 1625   wcel 1686   wne 2448   wnel 2449  wral 2545  wrex 2546  cvv 2790   wss 3154  c0 3457   class class class wbr 4025   cmpt 4079   cep 4305   wfr 4351   csuc 4396  com 4658   cdm 4691   crn 4692   wfn 5252  cfv 5257 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pr 4216  ax-un 4514  ax-reg 7308  ax-inf2 7344 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265
 Copyright terms: Public domain W3C validator