Theorem soss 5570

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ w3o 1086  ∀wral 3060   ⊆ wss 3913   class class class wbr 5110   Po wpo 5548   Or wor 5549

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-v 3448  df-in 3920  df-ss 3930  df-po 5550  df-so 5551

This theorem is referenced by:  soeq2  5572  wess  5625  wereu  5634  wereu2  5635  ordunifi  9244  fisup2g  9413  fisupcl  9414  fiinf2g  9445  ordtypelem8  9470  wemapso2lem  9497  iunfictbso  10059  fin1a2lem10  10354  fin1a2lem11  10355  zornn0g  10450  ltsopi  10833  npomex  10941  fimaxre  12108  fiminre  12111  suprfinzcl  12626  isercolllem1  15561  summolem2  15612  zsum  15614  prodmolem2  15829  zprod  15831  gsumval3  19698  iccpnfhmeo  24345  xrhmeo  24346  dvgt0lem2  25404  dgrval  25626  dgrcl  25631  dgrub  25632  dgrlb  25634  aannenlem3  25727  logccv  26055  nomaxmo  27083  nominmo  27084  xrge0infssd  31734  infxrge0lb  31737  infxrge0glb  31738  infxrge0gelb  31739  ssnnssfz  31758  xrge0iifiso  32605  omsfval  32983  omsf  32985  oms0  32986  omssubaddlem  32988  omssubadd  32989  oddpwdc  33043  erdszelem4  33875  erdszelem8  33879  erdsze2lem1  33884  erdsze2lem2  33885  supfz  34387  inffz  34388  finorwe  35926  fin2so  36138  sticksstones3  40629  rencldnfilem  41201  fzisoeu  43655  fourierdlem36  44504  ssnn0ssfz  46545