Theorem soss 5457

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.

Step	Hyp	Ref	Expression
1		poss 5440	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
2		ss2ralv 3983	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3	1, 2	anim12d 611	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
4		df-so 5439	. 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5		df-so 5439	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
6	3, 4, 5	3imtr4g 299	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))

Syntax hints:   → wi 4   ∧ wa 399   ∨ w3o 1083  ∀wral 3106   ⊆ wss 3881   class class class wbr 5030   Po wpo 5436   Or wor 5437

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-v 3443  df-in 3888  df-ss 3898  df-po 5438  df-so 5439

This theorem is referenced by:  soeq2  5459  wess  5506  wereu  5515  wereu2  5516  ordunifi  8752  fisup2g  8916  fisupcl  8917  fiinf2g  8948  ordtypelem8  8973  wemapso2lem  9000  iunfictbso  9525  fin1a2lem10  9820  fin1a2lem11  9821  zornn0g  9916  ltsopi  10299  npomex  10407  fimaxre  11573  fiminre  11576  suprfinzcl  12085  isercolllem1  15013  summolem2  15065  zsum  15067  prodmolem2  15281  zprod  15283  gsumval3  19020  iccpnfhmeo  23550  xrhmeo  23551  dvgt0lem2  24606  dgrval  24825  dgrcl  24830  dgrub  24831  dgrlb  24833  aannenlem3  24926  logccv  25254  xrge0infssd  30511  infxrge0lb  30514  infxrge0glb  30515  infxrge0gelb  30516  ssnnssfz  30536  xrge0iifiso  31288  omsfval  31662  omsf  31664  oms0  31665  omssubaddlem  31667  omssubadd  31668  oddpwdc  31722  erdszelem4  32554  erdszelem8  32558  erdsze2lem1  32563  erdsze2lem2  32564  supfz  33073  inffz  33074  nomaxmo  33314  finorwe  34799  fin2so  35044  rencldnfilem  39761  fzisoeu  41932  fourierdlem36  42785  ssnn0ssfz  44751