Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  wsuccl Structured version   Visualization version   GIF version

Theorem wsuccl 34787
Description: If 𝑋 is a set with an 𝑅 successor in 𝐴, then its well-founded successor is a member of 𝐴. (Contributed by Scott Fenton, 15-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.)
Hypotheses
Ref Expression
wsuccl.1 (𝜑𝑅 We 𝐴)
wsuccl.2 (𝜑𝑅 Se 𝐴)
wsuccl.3 (𝜑𝑋𝑉)
wsuccl.4 (𝜑 → ∃𝑦𝐴 𝑋𝑅𝑦)
Assertion
Ref Expression
wsuccl (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ 𝐴)
Distinct variable groups:   𝑦,𝑅   𝑦,𝐴   𝑦,𝑋
Allowed substitution hints:   𝜑(𝑦)   𝑉(𝑦)

Proof of Theorem wsuccl
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-wsuc 34772 . 2 wsuc(𝑅, 𝐴, 𝑋) = inf(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅)
2 wsuccl.1 . . . 4 (𝜑𝑅 We 𝐴)
3 weso 5666 . . . 4 (𝑅 We 𝐴𝑅 Or 𝐴)
42, 3syl 17 . . 3 (𝜑𝑅 Or 𝐴)
5 wsuccl.2 . . . 4 (𝜑𝑅 Se 𝐴)
6 wsuccl.3 . . . 4 (𝜑𝑋𝑉)
7 wsuccl.4 . . . 4 (𝜑 → ∃𝑦𝐴 𝑋𝑅𝑦)
82, 5, 6, 7wsuclem 34785 . . 3 (𝜑 → ∃𝑎𝐴 (∀𝑏 ∈ Pred (𝑅, 𝐴, 𝑋) ¬ 𝑏𝑅𝑎 ∧ ∀𝑏𝐴 (𝑎𝑅𝑏 → ∃𝑐 ∈ Pred (𝑅, 𝐴, 𝑋)𝑐𝑅𝑏)))
94, 8infcl 9479 . 2 (𝜑 → inf(Pred(𝑅, 𝐴, 𝑋), 𝐴, 𝑅) ∈ 𝐴)
101, 9eqeltrid 2837 1 (𝜑 → wsuc(𝑅, 𝐴, 𝑋) ∈ 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wrex 3070   class class class wbr 5147   Or wor 5586   Se wse 5628   We wwe 5629  ccnv 5674  Predcpred 6296  infcinf 9432  wsuccwsuc 34770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-iota 6492  df-riota 7361  df-sup 9433  df-inf 9434  df-wsuc 34772
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator