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

Theorem noinfep 8417
Description: Using the Axiom of Regularity in the form zfregfr 8369, 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 𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹𝑥)
Distinct variable group:   𝑥,𝐹

Proof of Theorem noinfep
Dummy variables 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 omex 8400 . . . . 5 ω ∈ V
21mptex 6368 . . . 4 (𝑤 ∈ ω ↦ (𝐹𝑤)) ∈ V
32rnex 6969 . . 3 ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ∈ V
4 zfregfr 8369 . . 3 E Fr ran (𝑤 ∈ ω ↦ (𝐹𝑤))
5 ssid 3586 . . 3 ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ⊆ ran (𝑤 ∈ ω ↦ (𝐹𝑤))
6 dmmptg 5535 . . . . . 6 (∀𝑤 ∈ ω (𝐹𝑤) ∈ V → dom (𝑤 ∈ ω ↦ (𝐹𝑤)) = ω)
7 fvex 6098 . . . . . . 7 (𝐹𝑤) ∈ V
87a1i 11 . . . . . 6 (𝑤 ∈ ω → (𝐹𝑤) ∈ V)
96, 8mprg 2909 . . . . 5 dom (𝑤 ∈ ω ↦ (𝐹𝑤)) = ω
10 peano1 6954 . . . . . 6 ∅ ∈ ω
1110ne0ii 3881 . . . . 5 ω ≠ ∅
129, 11eqnetri 2851 . . . 4 dom (𝑤 ∈ ω ↦ (𝐹𝑤)) ≠ ∅
13 dm0rn0 5250 . . . . 5 (dom (𝑤 ∈ ω ↦ (𝐹𝑤)) = ∅ ↔ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) = ∅)
1413necon3bii 2833 . . . 4 (dom (𝑤 ∈ ω ↦ (𝐹𝑤)) ≠ ∅ ↔ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ≠ ∅)
1512, 14mpbi 218 . . 3 ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ≠ ∅
16 fri 4990 . . 3 (((ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ∈ V ∧ E Fr ran (𝑤 ∈ ω ↦ (𝐹𝑤))) ∧ (ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ⊆ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ∧ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ≠ ∅)) → ∃𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤))∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ¬ 𝑧 E 𝑦)
173, 4, 5, 15, 16mp4an 704 . 2 𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤))∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ¬ 𝑧 E 𝑦
18 eqid 2609 . . . . . . 7 (𝑤 ∈ ω ↦ (𝐹𝑤)) = (𝑤 ∈ ω ↦ (𝐹𝑤))
197, 18fnmpti 5921 . . . . . 6 (𝑤 ∈ ω ↦ (𝐹𝑤)) Fn ω
20 fvelrnb 6138 . . . . . 6 ((𝑤 ∈ ω ↦ (𝐹𝑤)) Fn ω → (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ↔ ∃𝑥 ∈ ω ((𝑤 ∈ ω ↦ (𝐹𝑤))‘𝑥) = 𝑦))
2119, 20ax-mp 5 . . . . 5 (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ↔ ∃𝑥 ∈ ω ((𝑤 ∈ ω ↦ (𝐹𝑤))‘𝑥) = 𝑦)
22 peano2 6955 . . . . . . . . . . 11 (𝑥 ∈ ω → suc 𝑥 ∈ ω)
23 fveq2 6088 . . . . . . . . . . . 12 (𝑤 = suc 𝑥 → (𝐹𝑤) = (𝐹‘suc 𝑥))
24 fvex 6098 . . . . . . . . . . . 12 (𝐹‘suc 𝑥) ∈ V
2523, 18, 24fvmpt 6176 . . . . . . . . . . 11 (suc 𝑥 ∈ ω → ((𝑤 ∈ ω ↦ (𝐹𝑤))‘suc 𝑥) = (𝐹‘suc 𝑥))
2622, 25syl 17 . . . . . . . . . 10 (𝑥 ∈ ω → ((𝑤 ∈ ω ↦ (𝐹𝑤))‘suc 𝑥) = (𝐹‘suc 𝑥))
27 fnfvelrn 6249 . . . . . . . . . . 11 (((𝑤 ∈ ω ↦ (𝐹𝑤)) Fn ω ∧ suc 𝑥 ∈ ω) → ((𝑤 ∈ ω ↦ (𝐹𝑤))‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)))
2819, 22, 27sylancr 693 . . . . . . . . . 10 (𝑥 ∈ ω → ((𝑤 ∈ ω ↦ (𝐹𝑤))‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)))
2926, 28eqeltrrd 2688 . . . . . . . . 9 (𝑥 ∈ ω → (𝐹‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)))
30 epel 4942 . . . . . . . . . . . . 13 (𝑧 E 𝑦𝑧𝑦)
31 eleq1 2675 . . . . . . . . . . . . 13 (𝑧 = (𝐹‘suc 𝑥) → (𝑧𝑦 ↔ (𝐹‘suc 𝑥) ∈ 𝑦))
3230, 31syl5bb 270 . . . . . . . . . . . 12 (𝑧 = (𝐹‘suc 𝑥) → (𝑧 E 𝑦 ↔ (𝐹‘suc 𝑥) ∈ 𝑦))
3332notbid 306 . . . . . . . . . . 11 (𝑧 = (𝐹‘suc 𝑥) → (¬ 𝑧 E 𝑦 ↔ ¬ (𝐹‘suc 𝑥) ∈ 𝑦))
34 df-nel 2782 . . . . . . . . . . 11 ((𝐹‘suc 𝑥) ∉ 𝑦 ↔ ¬ (𝐹‘suc 𝑥) ∈ 𝑦)
3533, 34syl6bbr 276 . . . . . . . . . 10 (𝑧 = (𝐹‘suc 𝑥) → (¬ 𝑧 E 𝑦 ↔ (𝐹‘suc 𝑥) ∉ 𝑦))
3635rspccv 3278 . . . . . . . . 9 (∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ¬ 𝑧 E 𝑦 → ((𝐹‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) → (𝐹‘suc 𝑥) ∉ 𝑦))
3729, 36syl5com 31 . . . . . . . 8 (𝑥 ∈ ω → (∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ¬ 𝑧 E 𝑦 → (𝐹‘suc 𝑥) ∉ 𝑦))
38 fveq2 6088 . . . . . . . . . . . 12 (𝑤 = 𝑥 → (𝐹𝑤) = (𝐹𝑥))
39 fvex 6098 . . . . . . . . . . . 12 (𝐹𝑥) ∈ V
4038, 18, 39fvmpt 6176 . . . . . . . . . . 11 (𝑥 ∈ ω → ((𝑤 ∈ ω ↦ (𝐹𝑤))‘𝑥) = (𝐹𝑥))
41 eqeq1 2613 . . . . . . . . . . 11 (((𝑤 ∈ ω ↦ (𝐹𝑤))‘𝑥) = 𝑦 → (((𝑤 ∈ ω ↦ (𝐹𝑤))‘𝑥) = (𝐹𝑥) ↔ 𝑦 = (𝐹𝑥)))
4240, 41syl5ibcom 233 . . . . . . . . . 10 (𝑥 ∈ ω → (((𝑤 ∈ ω ↦ (𝐹𝑤))‘𝑥) = 𝑦𝑦 = (𝐹𝑥)))
43 neleq2 2888 . . . . . . . . . . 11 (𝑦 = (𝐹𝑥) → ((𝐹‘suc 𝑥) ∉ 𝑦 ↔ (𝐹‘suc 𝑥) ∉ (𝐹𝑥)))
4443biimpd 217 . . . . . . . . . 10 (𝑦 = (𝐹𝑥) → ((𝐹‘suc 𝑥) ∉ 𝑦 → (𝐹‘suc 𝑥) ∉ (𝐹𝑥)))
4542, 44syl6 34 . . . . . . . . 9 (𝑥 ∈ ω → (((𝑤 ∈ ω ↦ (𝐹𝑤))‘𝑥) = 𝑦 → ((𝐹‘suc 𝑥) ∉ 𝑦 → (𝐹‘suc 𝑥) ∉ (𝐹𝑥))))
4645com23 83 . . . . . . . 8 (𝑥 ∈ ω → ((𝐹‘suc 𝑥) ∉ 𝑦 → (((𝑤 ∈ ω ↦ (𝐹𝑤))‘𝑥) = 𝑦 → (𝐹‘suc 𝑥) ∉ (𝐹𝑥))))
4737, 46syld 45 . . . . . . 7 (𝑥 ∈ ω → (∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ¬ 𝑧 E 𝑦 → (((𝑤 ∈ ω ↦ (𝐹𝑤))‘𝑥) = 𝑦 → (𝐹‘suc 𝑥) ∉ (𝐹𝑥))))
4847com12 32 . . . . . 6 (∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ¬ 𝑧 E 𝑦 → (𝑥 ∈ ω → (((𝑤 ∈ ω ↦ (𝐹𝑤))‘𝑥) = 𝑦 → (𝐹‘suc 𝑥) ∉ (𝐹𝑥))))
4948reximdvai 2997 . . . . 5 (∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ¬ 𝑧 E 𝑦 → (∃𝑥 ∈ ω ((𝑤 ∈ ω ↦ (𝐹𝑤))‘𝑥) = 𝑦 → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹𝑥)))
5021, 49syl5bi 230 . . . 4 (∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ¬ 𝑧 E 𝑦 → (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹𝑥)))
5150com12 32 . . 3 (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) → (∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ¬ 𝑧 E 𝑦 → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹𝑥)))
5251rexlimiv 3008 . 2 (∃𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤))∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹𝑤)) ¬ 𝑧 E 𝑦 → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹𝑥))
5317, 52ax-mp 5 1 𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194   = wceq 1474  wcel 1976  wne 2779  wnel 2780  wral 2895  wrex 2896  Vcvv 3172  wss 3539  c0 3873   class class class wbr 4577  cmpt 4637   E cep 4937   Fr wfr 4984  dom cdm 5028  ran crn 5029  suc csuc 5628   Fn wfn 5785  cfv 5790  ωcom 6934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pr 4828  ax-un 6824  ax-reg 8357  ax-inf2 8398
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-om 6935
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator