Theorem soss 5551

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085  ∀wral 3044   ⊆ wss 3905   class class class wbr 5095   Po wpo 5529   Or wor 5530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045  df-ss 3922  df-po 5531  df-so 5532

This theorem is referenced by:  soeq2  5553  wess  5609  wereu  5619  wereu2  5620  ordunifi  9195  fisup2g  9378  fisupcl  9379  fiinf2g  9411  ordtypelem8  9436  wemapso2lem  9463  iunfictbso  10027  fin1a2lem10  10322  fin1a2lem11  10323  zornn0g  10418  ltsopi  10801  npomex  10909  fimaxre  12087  fiminre  12090  suprfinzcl  12608  isercolllem1  15590  summolem2  15641  zsum  15643  prodmolem2  15860  zprod  15862  gsumval3  19804  iccpnfhmeo  24859  xrhmeo  24860  dvgt0lem2  25924  dgrval  26149  dgrcl  26154  dgrub  26155  dgrlb  26157  aannenlem3  26254  logccv  26588  nomaxmo  27626  nominmo  27627  n0sfincut  28269  xrge0infssd  32717  infxrge0lb  32720  infxrge0glb  32721  infxrge0gelb  32722  ssnnssfz  32743  xrge0iifiso  33901  omsfval  34261  omsf  34263  oms0  34264  omssubaddlem  34266  omssubadd  34267  oddpwdc  34321  erdszelem4  35166  erdszelem8  35170  erdsze2lem1  35175  erdsze2lem2  35176  supfz  35701  inffz  35702  finorwe  37355  fin2so  37586  sticksstones3  42121  rencldnfilem  42793  fzisoeu  45282  fourierdlem36  46125  ssnn0ssfz  48334