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

Theorem rankwflemb 8904
Description: Two ways of saying a set is well-founded. (Contributed by NM, 11-Oct-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
Assertion
Ref Expression
rankwflemb (𝐴 (𝑅1 “ On) ↔ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
Distinct variable group:   𝑥,𝐴

Proof of Theorem rankwflemb
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eluni 4629 . . 3 (𝐴 (𝑅1 “ On) ↔ ∃𝑦(𝐴𝑦𝑦 ∈ (𝑅1 “ On)))
2 r1funlim 8877 . . . . . . . 8 (Fun 𝑅1 ∧ Lim dom 𝑅1)
32simpli 477 . . . . . . 7 Fun 𝑅1
4 fvelima 6471 . . . . . . 7 ((Fun 𝑅1𝑦 ∈ (𝑅1 “ On)) → ∃𝑥 ∈ On (𝑅1𝑥) = 𝑦)
53, 4mpan 682 . . . . . 6 (𝑦 ∈ (𝑅1 “ On) → ∃𝑥 ∈ On (𝑅1𝑥) = 𝑦)
6 eleq2 2865 . . . . . . . . 9 ((𝑅1𝑥) = 𝑦 → (𝐴 ∈ (𝑅1𝑥) ↔ 𝐴𝑦))
76biimprcd 242 . . . . . . . 8 (𝐴𝑦 → ((𝑅1𝑥) = 𝑦𝐴 ∈ (𝑅1𝑥)))
8 r1tr 8887 . . . . . . . . . . . 12 Tr (𝑅1𝑥)
9 trss 4952 . . . . . . . . . . . 12 (Tr (𝑅1𝑥) → (𝐴 ∈ (𝑅1𝑥) → 𝐴 ⊆ (𝑅1𝑥)))
108, 9ax-mp 5 . . . . . . . . . . 11 (𝐴 ∈ (𝑅1𝑥) → 𝐴 ⊆ (𝑅1𝑥))
11 elpwg 4355 . . . . . . . . . . 11 (𝐴 ∈ (𝑅1𝑥) → (𝐴 ∈ 𝒫 (𝑅1𝑥) ↔ 𝐴 ⊆ (𝑅1𝑥)))
1210, 11mpbird 249 . . . . . . . . . 10 (𝐴 ∈ (𝑅1𝑥) → 𝐴 ∈ 𝒫 (𝑅1𝑥))
13 elfvdm 6441 . . . . . . . . . . 11 (𝐴 ∈ (𝑅1𝑥) → 𝑥 ∈ dom 𝑅1)
14 r1sucg 8880 . . . . . . . . . . 11 (𝑥 ∈ dom 𝑅1 → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
1513, 14syl 17 . . . . . . . . . 10 (𝐴 ∈ (𝑅1𝑥) → (𝑅1‘suc 𝑥) = 𝒫 (𝑅1𝑥))
1612, 15eleqtrrd 2879 . . . . . . . . 9 (𝐴 ∈ (𝑅1𝑥) → 𝐴 ∈ (𝑅1‘suc 𝑥))
1716a1i 11 . . . . . . . 8 (𝑥 ∈ On → (𝐴 ∈ (𝑅1𝑥) → 𝐴 ∈ (𝑅1‘suc 𝑥)))
187, 17syl9 77 . . . . . . 7 (𝐴𝑦 → (𝑥 ∈ On → ((𝑅1𝑥) = 𝑦𝐴 ∈ (𝑅1‘suc 𝑥))))
1918reximdvai 3193 . . . . . 6 (𝐴𝑦 → (∃𝑥 ∈ On (𝑅1𝑥) = 𝑦 → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥)))
205, 19syl5 34 . . . . 5 (𝐴𝑦 → (𝑦 ∈ (𝑅1 “ On) → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥)))
2120imp 396 . . . 4 ((𝐴𝑦𝑦 ∈ (𝑅1 “ On)) → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
2221exlimiv 2026 . . 3 (∃𝑦(𝐴𝑦𝑦 ∈ (𝑅1 “ On)) → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
231, 22sylbi 209 . 2 (𝐴 (𝑅1 “ On) → ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
24 elfvdm 6441 . . . . . 6 (𝐴 ∈ (𝑅1‘suc 𝑥) → suc 𝑥 ∈ dom 𝑅1)
25 fvelrn 6576 . . . . . 6 ((Fun 𝑅1 ∧ suc 𝑥 ∈ dom 𝑅1) → (𝑅1‘suc 𝑥) ∈ ran 𝑅1)
263, 24, 25sylancr 582 . . . . 5 (𝐴 ∈ (𝑅1‘suc 𝑥) → (𝑅1‘suc 𝑥) ∈ ran 𝑅1)
27 df-ima 5323 . . . . . 6 (𝑅1 “ On) = ran (𝑅1 ↾ On)
28 funrel 6116 . . . . . . . . 9 (Fun 𝑅1 → Rel 𝑅1)
293, 28ax-mp 5 . . . . . . . 8 Rel 𝑅1
302simpri 480 . . . . . . . . 9 Lim dom 𝑅1
31 limord 5998 . . . . . . . . 9 (Lim dom 𝑅1 → Ord dom 𝑅1)
32 ordsson 7221 . . . . . . . . 9 (Ord dom 𝑅1 → dom 𝑅1 ⊆ On)
3330, 31, 32mp2b 10 . . . . . . . 8 dom 𝑅1 ⊆ On
34 relssres 5646 . . . . . . . 8 ((Rel 𝑅1 ∧ dom 𝑅1 ⊆ On) → (𝑅1 ↾ On) = 𝑅1)
3529, 33, 34mp2an 684 . . . . . . 7 (𝑅1 ↾ On) = 𝑅1
3635rneqi 5553 . . . . . 6 ran (𝑅1 ↾ On) = ran 𝑅1
3727, 36eqtri 2819 . . . . 5 (𝑅1 “ On) = ran 𝑅1
3826, 37syl6eleqr 2887 . . . 4 (𝐴 ∈ (𝑅1‘suc 𝑥) → (𝑅1‘suc 𝑥) ∈ (𝑅1 “ On))
39 elunii 4631 . . . 4 ((𝐴 ∈ (𝑅1‘suc 𝑥) ∧ (𝑅1‘suc 𝑥) ∈ (𝑅1 “ On)) → 𝐴 (𝑅1 “ On))
4038, 39mpdan 679 . . 3 (𝐴 ∈ (𝑅1‘suc 𝑥) → 𝐴 (𝑅1 “ On))
4140rexlimivw 3208 . 2 (∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥) → 𝐴 (𝑅1 “ On))
4223, 41impbii 201 1 (𝐴 (𝑅1 “ On) ↔ ∃𝑥 ∈ On 𝐴 ∈ (𝑅1‘suc 𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385   = wceq 1653  wex 1875  wcel 2157  wrex 3088  wss 3767  𝒫 cpw 4347   cuni 4626  Tr wtr 4943  dom cdm 5310  ran crn 5311  cres 5312  cima 5313  Rel wrel 5315  Ord word 5938  Oncon0 5939  Lim wlim 5940  suc csuc 5941  Fun wfun 6093  cfv 6099  𝑅1cr1 8873
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-sep 4973  ax-nul 4981  ax-pow 5033  ax-pr 5095  ax-un 7181
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-ne 2970  df-ral 3092  df-rex 3093  df-reu 3094  df-rab 3096  df-v 3385  df-sbc 3632  df-csb 3727  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-pss 3783  df-nul 4114  df-if 4276  df-pw 4349  df-sn 4367  df-pr 4369  df-tp 4371  df-op 4373  df-uni 4627  df-iun 4710  df-br 4842  df-opab 4904  df-mpt 4921  df-tr 4944  df-id 5218  df-eprel 5223  df-po 5231  df-so 5232  df-fr 5269  df-we 5271  df-xp 5316  df-rel 5317  df-cnv 5318  df-co 5319  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323  df-pred 5896  df-ord 5942  df-on 5943  df-lim 5944  df-suc 5945  df-iota 6062  df-fun 6101  df-fn 6102  df-f 6103  df-f1 6104  df-fo 6105  df-f1o 6106  df-fv 6107  df-om 7298  df-wrecs 7643  df-recs 7705  df-rdg 7743  df-r1 8875
This theorem is referenced by:  rankf  8905  r1elwf  8907  rankvalb  8908  rankidb  8911  rankwflem  8926  tcrank  8995  dfac12r  9254
  Copyright terms: Public domain W3C validator