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

Theorem fiming 9297
Description: A finite set has a minimum under a total order. (Contributed by AV, 6-Oct-2020.)
Assertion
Ref Expression
fiming ((𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥𝑅𝑦))
Distinct variable groups:   𝑥,𝑅,𝑦   𝑥,𝐴,𝑦

Proof of Theorem fiming
StepHypRef Expression
1 fimin2g 9296 . 2 ((𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥𝐴𝑦𝐴 ¬ 𝑦𝑅𝑥)
2 nesym 2998 . . . . . . . . 9 (𝑥𝑦 ↔ ¬ 𝑦 = 𝑥)
32imbi1i 351 . . . . . . . 8 ((𝑥𝑦𝑥𝑅𝑦) ↔ (¬ 𝑦 = 𝑥𝑥𝑅𝑦))
4 pm4.64 847 . . . . . . . 8 ((¬ 𝑦 = 𝑥𝑥𝑅𝑦) ↔ (𝑦 = 𝑥𝑥𝑅𝑦))
53, 4bitri 276 . . . . . . 7 ((𝑥𝑦𝑥𝑅𝑦) ↔ (𝑦 = 𝑥𝑥𝑅𝑦))
6 sotric 5538 . . . . . . . . 9 ((𝑅 Or 𝐴 ∧ (𝑦𝐴𝑥𝐴)) → (𝑦𝑅𝑥 ↔ ¬ (𝑦 = 𝑥𝑥𝑅𝑦)))
76ancom2s 648 . . . . . . . 8 ((𝑅 Or 𝐴 ∧ (𝑥𝐴𝑦𝐴)) → (𝑦𝑅𝑥 ↔ ¬ (𝑦 = 𝑥𝑥𝑅𝑦)))
87con2bid 356 . . . . . . 7 ((𝑅 Or 𝐴 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑦 = 𝑥𝑥𝑅𝑦) ↔ ¬ 𝑦𝑅𝑥))
95, 8bitrid 284 . . . . . 6 ((𝑅 Or 𝐴 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑥𝑦𝑥𝑅𝑦) ↔ ¬ 𝑦𝑅𝑥))
109anassrs 469 . . . . 5 (((𝑅 Or 𝐴𝑥𝐴) ∧ 𝑦𝐴) → ((𝑥𝑦𝑥𝑅𝑦) ↔ ¬ 𝑦𝑅𝑥))
1110ralbidva 3169 . . . 4 ((𝑅 Or 𝐴𝑥𝐴) → (∀𝑦𝐴 (𝑥𝑦𝑥𝑅𝑦) ↔ ∀𝑦𝐴 ¬ 𝑦𝑅𝑥))
1211rexbidva 3170 . . 3 (𝑅 Or 𝐴 → (∃𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥𝑅𝑦) ↔ ∃𝑥𝐴𝑦𝐴 ¬ 𝑦𝑅𝑥))
13123ad2ant1 1133 . 2 ((𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → (∃𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥𝑅𝑦) ↔ ∃𝑥𝐴𝑦𝐴 ¬ 𝑦𝑅𝑥))
141, 13mpbird 258 1 ((𝑅 Or 𝐴𝐴 ∈ Fin ∧ 𝐴 ≠ ∅) → ∃𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥𝑅𝑦))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  wo 845  w3a 1087  wcel 2104  wne 2941  wral 3062  wrex 3071  c0 4262   class class class wbr 5081   Or wor 5509  Fincfn 8760
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-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-un 7616
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3286  df-rab 3287  df-v 3439  df-sbc 3722  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-pss 3911  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-tr 5199  df-id 5496  df-eprel 5502  df-po 5510  df-so 5511  df-fr 5551  df-we 5553  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-rn 5607  df-res 5608  df-ima 5609  df-ord 6280  df-on 6281  df-lim 6282  df-suc 6283  df-iota 6406  df-fun 6456  df-fn 6457  df-f 6458  df-f1 6459  df-fo 6460  df-f1o 6461  df-fv 6462  df-om 7741  df-en 8761  df-fin 8764
This theorem is referenced by:  fiinfg  9298  fiminre  11964
  Copyright terms: Public domain W3C validator