Theorem soss 5552

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085  ∀wral 3051   ⊆ wss 3901   class class class wbr 5098   Po wpo 5530   Or wor 5531

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 3052  df-ss 3918  df-po 5532  df-so 5533

This theorem is referenced by:  soeq2  5554  wess  5610  wereu  5620  wereu2  5621  ordunifi  9190  fisup2g  9372  fisupcl  9373  fiinf2g  9405  ordtypelem8  9430  wemapso2lem  9457  iunfictbso  10024  fin1a2lem10  10319  fin1a2lem11  10320  zornn0g  10415  ltsopi  10799  npomex  10907  fimaxre  12086  fiminre  12089  suprfinzcl  12606  isercolllem1  15588  summolem2  15639  zsum  15641  prodmolem2  15858  zprod  15860  gsumval3  19836  iccpnfhmeo  24899  xrhmeo  24900  dvgt0lem2  25964  dgrval  26189  dgrcl  26194  dgrub  26195  dgrlb  26197  aannenlem3  26294  logccv  26628  nomaxmo  27666  nominmo  27667  n0fincut  28351  bdayfinbndlem1  28463  xrge0infssd  32841  infxrge0lb  32844  infxrge0glb  32845  infxrge0gelb  32846  ssnnssfz  32867  xrge0iifiso  34092  omsfval  34451  omsf  34453  oms0  34454  omssubaddlem  34456  omssubadd  34457  oddpwdc  34511  erdszelem4  35388  erdszelem8  35392  erdsze2lem1  35397  erdsze2lem2  35398  supfz  35923  inffz  35924  finorwe  37583  fin2so  37804  sticksstones3  42398  rencldnfilem  43058  fzisoeu  45544  fourierdlem36  46383  ssnn0ssfz  48591