Theorem soss 5628

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1086  ∀wral 3067   ⊆ wss 3976   class class class wbr 5166   Po wpo 5605   Or wor 5606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3068  df-ss 3993  df-po 5607  df-so 5608

This theorem is referenced by:  soeq2  5630  wess  5686  wereu  5696  wereu2  5697  ordunifi  9354  fisup2g  9537  fisupcl  9538  fiinf2g  9569  ordtypelem8  9594  wemapso2lem  9621  iunfictbso  10183  fin1a2lem10  10478  fin1a2lem11  10479  zornn0g  10574  ltsopi  10957  npomex  11065  fimaxre  12239  fiminre  12242  suprfinzcl  12757  isercolllem1  15713  summolem2  15764  zsum  15766  prodmolem2  15983  zprod  15985  gsumval3  19949  iccpnfhmeo  24995  xrhmeo  24996  dvgt0lem2  26062  dgrval  26287  dgrcl  26292  dgrub  26293  dgrlb  26295  aannenlem3  26390  logccv  26723  nomaxmo  27761  nominmo  27762  xrge0infssd  32768  infxrge0lb  32771  infxrge0glb  32772  infxrge0gelb  32773  ssnnssfz  32792  xrge0iifiso  33881  omsfval  34259  omsf  34261  oms0  34262  omssubaddlem  34264  omssubadd  34265  oddpwdc  34319  erdszelem4  35162  erdszelem8  35166  erdsze2lem1  35171  erdsze2lem2  35172  supfz  35691  inffz  35692  finorwe  37348  fin2so  37567  sticksstones3  42105  rencldnfilem  42776  fzisoeu  45215  fourierdlem36  46064  ssnn0ssfz  48074