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

Theorem soss 5082
Description: Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
soss (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))

Proof of Theorem soss
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poss 5066 . . 3 (𝐴𝐵 → (𝑅 Po 𝐵𝑅 Po 𝐴))
2 ssel 3630 . . . . . . 7 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
3 ssel 3630 . . . . . . 7 (𝐴𝐵 → (𝑦𝐴𝑦𝐵))
42, 3anim12d 585 . . . . . 6 (𝐴𝐵 → ((𝑥𝐴𝑦𝐴) → (𝑥𝐵𝑦𝐵)))
54imim1d 82 . . . . 5 (𝐴𝐵 → (((𝑥𝐵𝑦𝐵) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → ((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
652alimdv 1887 . . . 4 (𝐴𝐵 → (∀𝑥𝑦((𝑥𝐵𝑦𝐵) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
7 r2al 2968 . . . 4 (∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑥𝑦((𝑥𝐵𝑦𝐵) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
8 r2al 2968 . . . 4 (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
96, 7, 83imtr4g 285 . . 3 (𝐴𝐵 → (∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
101, 9anim12d 585 . 2 (𝐴𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))))
11 df-so 5065 . 2 (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
12 df-so 5065 . 2 (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥)))
1310, 11, 123imtr4g 285 1 (𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3o 1053  wal 1521  wcel 2030  wral 2941  wss 3607   class class class wbr 4685   Po wpo 5062   Or wor 5063
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-in 3614  df-ss 3621  df-po 5064  df-so 5065
This theorem is referenced by:  soeq2  5084  wess  5130  wereu  5139  wereu2  5140  ordunifi  8251  fisup2g  8415  fisupcl  8416  fiinf2g  8447  ordtypelem8  8471  wemapso2lem  8498  iunfictbso  8975  fin1a2lem10  9269  fin1a2lem11  9270  zornn0g  9365  ltsopi  9748  npomex  9856  fimaxre  11006  suprfinzcl  11530  isercolllem1  14439  summolem2  14491  zsum  14493  prodmolem2  14709  zprod  14711  gsumval3  18354  iccpnfhmeo  22791  xrhmeo  22792  dvgt0lem2  23811  dgrval  24029  dgrcl  24034  dgrub  24035  dgrlb  24037  aannenlem3  24130  logccv  24454  xrge0infssd  29654  infxrge0lb  29657  infxrge0glb  29658  infxrge0gelb  29659  ssnnssfz  29677  xrge0iifiso  30109  omsfval  30484  omsf  30486  oms0  30487  omssubaddlem  30489  omssubadd  30490  oddpwdc  30544  erdszelem4  31302  erdszelem8  31306  erdsze2lem1  31311  erdsze2lem2  31312  supfz  31739  inffz  31740  inffzOLD  31741  nomaxmo  31972  fin2so  33526  rencldnfilem  37701  fzisoeu  39828  fourierdlem36  40678  ssnn0ssfz  42452
  Copyright terms: Public domain W3C validator