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

Theorem frinfm 36908
Description: A subset of a well-founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
frinfm ((𝑅 Fr 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
Distinct variable groups:   𝑥,𝑅,𝑦,𝑧   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦
Allowed substitution hint:   𝐶(𝑧)

Proof of Theorem frinfm
StepHypRef Expression
1 fri 5637 . . . . 5 (((𝐵𝐶𝑅 Fr 𝐴) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
21ancom1s 649 . . . 4 (((𝑅 Fr 𝐴𝐵𝐶) ∧ (𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
32exp43 435 . . 3 (𝑅 Fr 𝐴 → (𝐵𝐶 → (𝐵𝐴 → (𝐵 ≠ ∅ → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥))))
433imp2 1347 . 2 ((𝑅 Fr 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥)
5 ssel2 3978 . . . . . . . 8 ((𝐵𝐴𝑥𝐵) → 𝑥𝐴)
65adantrr 713 . . . . . . 7 ((𝐵𝐴 ∧ (𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦𝑅𝑥)) → 𝑥𝐴)
7 vex 3476 . . . . . . . . . . . 12 𝑥 ∈ V
8 vex 3476 . . . . . . . . . . . 12 𝑦 ∈ V
97, 8brcnv 5883 . . . . . . . . . . 11 (𝑥𝑅𝑦𝑦𝑅𝑥)
109biimpi 215 . . . . . . . . . 10 (𝑥𝑅𝑦𝑦𝑅𝑥)
1110con3i 154 . . . . . . . . 9 𝑦𝑅𝑥 → ¬ 𝑥𝑅𝑦)
1211ralimi 3081 . . . . . . . 8 (∀𝑦𝐵 ¬ 𝑦𝑅𝑥 → ∀𝑦𝐵 ¬ 𝑥𝑅𝑦)
1312ad2antll 725 . . . . . . 7 ((𝐵𝐴 ∧ (𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦𝑅𝑥)) → ∀𝑦𝐵 ¬ 𝑥𝑅𝑦)
14 breq2 5153 . . . . . . . . . . 11 (𝑧 = 𝑥 → (𝑦𝑅𝑧𝑦𝑅𝑥))
1514rspcev 3613 . . . . . . . . . 10 ((𝑥𝐵𝑦𝑅𝑥) → ∃𝑧𝐵 𝑦𝑅𝑧)
1615ex 411 . . . . . . . . 9 (𝑥𝐵 → (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))
1716ralrimivw 3148 . . . . . . . 8 (𝑥𝐵 → ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))
1817ad2antrl 724 . . . . . . 7 ((𝐵𝐴 ∧ (𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦𝑅𝑥)) → ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))
196, 13, 18jca32 514 . . . . . 6 ((𝐵𝐴 ∧ (𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦𝑅𝑥)) → (𝑥𝐴 ∧ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
2019ex 411 . . . . 5 (𝐵𝐴 → ((𝑥𝐵 ∧ ∀𝑦𝐵 ¬ 𝑦𝑅𝑥) → (𝑥𝐴 ∧ (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))))
2120reximdv2 3162 . . . 4 (𝐵𝐴 → (∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥 → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
2221adantl 480 . . 3 ((𝑅 Fr 𝐴𝐵𝐴) → (∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥 → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
23223ad2antr2 1187 . 2 ((𝑅 Fr 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → (∃𝑥𝐵𝑦𝐵 ¬ 𝑦𝑅𝑥 → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧))))
244, 23mpd 15 1 ((𝑅 Fr 𝐴 ∧ (𝐵𝐶𝐵𝐴𝐵 ≠ ∅)) → ∃𝑥𝐴 (∀𝑦𝐵 ¬ 𝑥𝑅𝑦 ∧ ∀𝑦𝐴 (𝑦𝑅𝑥 → ∃𝑧𝐵 𝑦𝑅𝑧)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  w3a 1085  wcel 2104  wne 2938  wral 3059  wrex 3068  wss 3949  c0 4323   class class class wbr 5149   Fr wfr 5629  ccnv 5676
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-fr 5632  df-cnv 5685
This theorem is referenced by:  welb  36909
  Copyright terms: Public domain W3C validator