Theorem soss 5547

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085  ∀wral 3048   ⊆ wss 3898   class class class wbr 5093   Po wpo 5525   Or wor 5526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3049  df-ss 3915  df-po 5527  df-so 5528

This theorem is referenced by:  soeq2  5549  wess  5605  wereu  5615  wereu2  5616  ordunifi  9181  fisup2g  9360  fisupcl  9361  fiinf2g  9393  ordtypelem8  9418  wemapso2lem  9445  iunfictbso  10012  fin1a2lem10  10307  fin1a2lem11  10308  zornn0g  10403  ltsopi  10786  npomex  10894  fimaxre  12073  fiminre  12076  suprfinzcl  12593  isercolllem1  15574  summolem2  15625  zsum  15627  prodmolem2  15844  zprod  15846  gsumval3  19821  iccpnfhmeo  24871  xrhmeo  24872  dvgt0lem2  25936  dgrval  26161  dgrcl  26166  dgrub  26167  dgrlb  26169  aannenlem3  26266  logccv  26600  nomaxmo  27638  nominmo  27639  n0sfincut  28283  xrge0infssd  32748  infxrge0lb  32751  infxrge0glb  32752  infxrge0gelb  32753  ssnnssfz  32774  xrge0iifiso  33969  omsfval  34328  omsf  34330  oms0  34331  omssubaddlem  34333  omssubadd  34334  oddpwdc  34388  erdszelem4  35259  erdszelem8  35263  erdsze2lem1  35268  erdsze2lem2  35269  supfz  35794  inffz  35795  finorwe  37447  fin2so  37667  sticksstones3  42261  rencldnfilem  42937  fzisoeu  45425  fourierdlem36  46265  ssnn0ssfz  48473