Theorem soss 5587

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 5569	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
2		ss2ralv 4005	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3	1, 2	anim12d 621	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
4		df-so 5568	. 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5		df-so 5568	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
6	3, 4, 5	3imtr4g 299	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ w3o 1102  ∀wral 3078   ⊆ wss 3902   class class class wbr 5107   Po wpo 5565   Or wor 5566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3079  df-ss 3919  df-po 5567  df-so 5568

This theorem is used by:  soeq2  5589  wess  5645  wereu  5655  wereu2  5656  ordunifi  9264  fisup2g  9443  fisupcl  9444  fiinf2g  9476  ordtypelem8  9501  wemapso2lem  9528  iunfictbso  10121  fin1a2lem10  10415  fin1a2lem11  10416  zornn0g  10511  ltsopi  10901  npomex  11009  fimaxre  12187  fiminre  12190  suprfinzcl  12739  isercolllem1  15756  summolem2  15806  zsum  15808  prodmolem2  16028  zprod  16030  gsumval3  20040  iccpnfhmeo  25179  xrhmeo  25180  dvgt0lem2  26237  dgrval  26461  dgrcl  26466  dgrub  26467  dgrlb  26469  aannenlem3  26573  logccv  26908  nomaxmo  27942  nominmo  27943  n0fincut  28628  bdayfinbndlem1  28740  xrge0infssd  33240  infxrge0lb  33243  infxrge0glb  33244  infxrge0gelb  33245  ssnnssfz  33266  xrge0iifiso  34453  omsfval  34813  omsf  34815  oms0  34816  omssubaddlem  34818  omssubadd  34819  oddpwdc  34873  erdszelem4  35781  erdszelem8  35785  erdsze2lem1  35790  erdsze2lem2  35791  supfz  36316  inffz  36317  finorwe  38144  fin2so  38369  sticksstones3  43022  rencldnfilem  43669  fzisoeu  46141  fourierdlem36  46979  ssnn0ssfz  49287