Theorem soss 5560

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 5542	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
2		ss2ralv 4006	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3	1, 2	anim12d 610	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
4		df-so 5541	. 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5		df-so 5541	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
6	3, 4, 5	3imtr4g 296	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1086  ∀wral 3052   ⊆ wss 3903   class class class wbr 5100   Po wpo 5538   Or wor 5539

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 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053  df-ss 3920  df-po 5540  df-so 5541

This theorem is referenced by:  soeq2  5562  wess  5618  wereu  5628  wereu2  5629  ordunifi  9202  fisup2g  9384  fisupcl  9385  fiinf2g  9417  ordtypelem8  9442  wemapso2lem  9469  iunfictbso  10036  fin1a2lem10  10331  fin1a2lem11  10332  zornn0g  10427  ltsopi  10811  npomex  10919  fimaxre  12098  fiminre  12101  suprfinzcl  12618  isercolllem1  15600  summolem2  15651  zsum  15653  prodmolem2  15870  zprod  15872  gsumval3  19848  iccpnfhmeo  24911  xrhmeo  24912  dvgt0lem2  25976  dgrval  26201  dgrcl  26206  dgrub  26207  dgrlb  26209  aannenlem3  26306  logccv  26640  nomaxmo  27678  nominmo  27679  n0fincut  28363  bdayfinbndlem1  28475  xrge0infssd  32851  infxrge0lb  32854  infxrge0glb  32855  infxrge0gelb  32856  ssnnssfz  32877  xrge0iifiso  34112  omsfval  34471  omsf  34473  oms0  34474  omssubaddlem  34476  omssubadd  34477  oddpwdc  34531  erdszelem4  35407  erdszelem8  35411  erdsze2lem1  35416  erdsze2lem2  35417  supfz  35942  inffz  35943  finorwe  37631  fin2so  37852  sticksstones3  42512  rencldnfilem  43171  fzisoeu  45656  fourierdlem36  46495  ssnn0ssfz  48703