Theorem soss 5566

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085  ∀wral 3044   ⊆ wss 3914   class class class wbr 5107   Po wpo 5544   Or wor 5545

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 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045  df-ss 3931  df-po 5546  df-so 5547

This theorem is referenced by:  soeq2  5568  wess  5624  wereu  5634  wereu2  5635  ordunifi  9237  fisup2g  9420  fisupcl  9421  fiinf2g  9453  ordtypelem8  9478  wemapso2lem  9505  iunfictbso  10067  fin1a2lem10  10362  fin1a2lem11  10363  zornn0g  10458  ltsopi  10841  npomex  10949  fimaxre  12127  fiminre  12130  suprfinzcl  12648  isercolllem1  15631  summolem2  15682  zsum  15684  prodmolem2  15901  zprod  15903  gsumval3  19837  iccpnfhmeo  24843  xrhmeo  24844  dvgt0lem2  25908  dgrval  26133  dgrcl  26138  dgrub  26139  dgrlb  26141  aannenlem3  26238  logccv  26572  nomaxmo  27610  nominmo  27611  n0sfincut  28246  xrge0infssd  32684  infxrge0lb  32687  infxrge0glb  32688  infxrge0gelb  32689  ssnnssfz  32710  xrge0iifiso  33925  omsfval  34285  omsf  34287  oms0  34288  omssubaddlem  34290  omssubadd  34291  oddpwdc  34345  erdszelem4  35181  erdszelem8  35185  erdsze2lem1  35190  erdsze2lem2  35191  supfz  35716  inffz  35717  finorwe  37370  fin2so  37601  sticksstones3  42136  rencldnfilem  42808  fzisoeu  45298  fourierdlem36  46141  ssnn0ssfz  48337