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 3993	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3	1, 2	anim12d 610	. 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 1086  ∀wral 3052   ⊆ wss 3890   class class class wbr 5086   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 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053  df-ss 3907  df-po 5532  df-so 5533

This theorem is referenced by:  soeq2  5554  wess  5610  wereu  5620  wereu2  5621  ordunifi  9193  fisup2g  9375  fisupcl  9376  fiinf2g  9408  ordtypelem8  9433  wemapso2lem  9460  iunfictbso  10027  fin1a2lem10  10322  fin1a2lem11  10323  zornn0g  10418  ltsopi  10802  npomex  10910  fimaxre  12091  fiminre  12094  suprfinzcl  12634  isercolllem1  15618  summolem2  15669  zsum  15671  prodmolem2  15891  zprod  15893  gsumval3  19873  iccpnfhmeo  24922  xrhmeo  24923  dvgt0lem2  25980  dgrval  26203  dgrcl  26208  dgrub  26209  dgrlb  26211  aannenlem3  26307  logccv  26640  nomaxmo  27676  nominmo  27677  n0fincut  28361  bdayfinbndlem1  28473  xrge0infssd  32849  infxrge0lb  32852  infxrge0glb  32853  infxrge0gelb  32854  ssnnssfz  32875  xrge0iifiso  34095  omsfval  34454  omsf  34456  oms0  34457  omssubaddlem  34459  omssubadd  34460  oddpwdc  34514  erdszelem4  35392  erdszelem8  35396  erdsze2lem1  35401  erdsze2lem2  35402  supfz  35927  inffz  35928  finorwe  37712  fin2so  37942  sticksstones3  42601  rencldnfilem  43266  fzisoeu  45751  fourierdlem36  46589  ssnn0ssfz  48837