Theorem soss 5514

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 5496	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
2		ss2ralv 3985	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3	1, 2	anim12d 608	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
4		df-so 5495	. 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5		df-so 5495	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
6	3, 4, 5	3imtr4g 295	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1084  ∀wral 3063   ⊆ wss 3883   class class class wbr 5070   Po wpo 5492   Or wor 5493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-v 3424  df-in 3890  df-ss 3900  df-po 5494  df-so 5495

This theorem is referenced by:  soeq2  5516  wess  5567  wereu  5576  wereu2  5577  ordunifi  8994  fisup2g  9157  fisupcl  9158  fiinf2g  9189  ordtypelem8  9214  wemapso2lem  9241  iunfictbso  9801  fin1a2lem10  10096  fin1a2lem11  10097  zornn0g  10192  ltsopi  10575  npomex  10683  fimaxre  11849  fiminre  11852  suprfinzcl  12365  isercolllem1  15304  summolem2  15356  zsum  15358  prodmolem2  15573  zprod  15575  gsumval3  19423  iccpnfhmeo  24014  xrhmeo  24015  dvgt0lem2  25072  dgrval  25294  dgrcl  25299  dgrub  25300  dgrlb  25302  aannenlem3  25395  logccv  25723  xrge0infssd  30986  infxrge0lb  30989  infxrge0glb  30990  infxrge0gelb  30991  ssnnssfz  31010  xrge0iifiso  31787  omsfval  32161  omsf  32163  oms0  32164  omssubaddlem  32166  omssubadd  32167  oddpwdc  32221  erdszelem4  33056  erdszelem8  33060  erdsze2lem1  33065  erdsze2lem2  33066  supfz  33600  inffz  33601  nomaxmo  33828  nominmo  33829  finorwe  35480  fin2so  35691  sticksstones3  40032  rencldnfilem  40558  fzisoeu  42729  fourierdlem36  43574  ssnn0ssfz  45573