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 36185
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 5620 . . . . . 6 (𝐵𝐴 → (𝑅 We 𝐴𝑅 We 𝐵))
21impcom 408 . . . . 5 ((𝑅 We 𝐴𝐵𝐴) → 𝑅 We 𝐵)
3 weso 5624 . . . . 5 (𝑅 We 𝐵𝑅 Or 𝐵)
42, 3syl 17 . . . 4 ((𝑅 We 𝐴𝐵𝐴) → 𝑅 Or 𝐵)
5 cnvso 6240 . . . 4 (𝑅 Or 𝐵𝑅 Or 𝐵)
64, 5sylib 217 . . 3 ((𝑅 We 𝐴𝐵𝐴) → 𝑅 Or 𝐵)
763ad2antr2 1189 . 2 ((𝑅 We 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Or 𝐵)
8 wefr 5623 . . . . 5 (𝑅 We 𝐵𝑅 Fr 𝐵)
92, 8syl 17 . . . 4 ((𝑅 We 𝐴𝐵𝐴) → 𝑅 Fr 𝐵)
1093ad2antr2 1189 . . 3 ((𝑅 We 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → 𝑅 Fr 𝐵)
11 ssidd 3967 . . . . 5 (𝐵𝐴𝐵𝐵)
12113anim2i 1153 . . . 4 ((𝐵𝐶𝐵𝐴𝐵 ≠ ∅) → (𝐵𝐶𝐵𝐵𝐵 ≠ ∅))
1312adantl 482 . . 3 ((𝑅 We 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → (𝐵𝐶𝐵𝐵𝐵 ≠ ∅))
14 frinfm 36184 . . 3 ((𝑅 Fr 𝐵 ∧ (𝐵𝐶𝐵𝐵𝐵 ≠ ∅)) → ∃𝑥𝐵 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
1510, 13, 14syl2anc 584 . 2 ((𝑅 We 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
167, 15jca 512 1 ((𝑅 We 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → (𝑅 Or 𝐵 ∧ ∃𝑥𝐵 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐵 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1087  wcel 2106  wne 2943  wral 3064  wrex 3073  wss 3910  c0 4282   class class class wbr 5105   Or wor 5544   Fr wfr 5585   We wwe 5587  ccnv 5632
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 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
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-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-br 5106  df-opab 5168  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-cnv 5641
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator