Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  welb Structured version   Visualization version   GIF version

Theorem welb 34010
Description: A nonempty subset of a well-ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
welb ((𝑅 We 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → (𝑅 Or 𝐵 ∧ ∃𝑥𝐵 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧

Proof of Theorem welb
StepHypRef Expression
1 wess 5297 . . . . . 6 (𝐵𝐴 → (𝑅 We 𝐴𝑅 We 𝐵))
21impcom 397 . . . . 5 ((𝑅 We 𝐴𝐵𝐴) → 𝑅 We 𝐵)
3 weso 5301 . . . . 5 (𝑅 We 𝐵𝑅 Or 𝐵)
42, 3syl 17 . . . 4 ((𝑅 We 𝐴𝐵𝐴) → 𝑅 Or 𝐵)
5 cnvso 5891 . . . 4 (𝑅 Or 𝐵𝑅 Or 𝐵)
64, 5sylib 210 . . 3 ((𝑅 We 𝐴𝐵𝐴) → 𝑅 Or 𝐵)
763ad2antr2 1241 . 2 ((𝑅 We 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Or 𝐵)
8 wefr 5300 . . . . 5 (𝑅 We 𝐵𝑅 Fr 𝐵)
92, 8syl 17 . . . 4 ((𝑅 We 𝐴𝐵𝐴) → 𝑅 Fr 𝐵)
1093ad2antr2 1241 . . 3 ((𝑅 We 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Fr 𝐵)
11 ssidd 3818 . . . . 5 (𝐵𝐴𝐵𝐵)
12113anim2i 1193 . . . 4 ((𝐵𝐶𝐵𝐴𝐵 ≠ ∅) → (𝐵𝐶𝐵𝐵𝐵 ≠ ∅))
1312adantl 474 . . 3 ((𝑅 We 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → (𝐵𝐶𝐵𝐵𝐵 ≠ ∅))
14 frinfm 34009 . . 3 ((𝑅 Fr 𝐵 ∧ (𝐵𝐶𝐵𝐵𝐵 ≠ ∅)) → ∃𝑥𝐵 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
1510, 13, 14syl2anc 580 . 2 ((𝑅 We 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
167, 15jca 508 1 ((𝑅 We 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → (𝑅 Or 𝐵 ∧ ∃𝑥𝐵 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 385  w3a 1108  wcel 2157  wne 2969  wral 3087  wrex 3088  wss 3767  c0 4113   class class class wbr 4841   Or wor 5230   Fr wfr 5266   We wwe 5268  ccnv 5309
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-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2375  ax-ext 2775  ax-sep 4973  ax-nul 4981  ax-pr 5095
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-rab 3096  df-v 3385  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-sn 4367  df-pr 4369  df-op 4373  df-br 4842  df-opab 4904  df-po 5231  df-so 5232  df-fr 5269  df-we 5271  df-cnv 5318
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator