Theorem soss 5594

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 5576	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
2		ss2ralv 4011	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3	1, 2	anim12d 621	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
4		df-so 5575	. 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5		df-so 5575	. 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 3082   ⊆ wss 3908   class class class wbr 5114   Po wpo 5572   Or wor 5573

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 3083  df-ss 3925  df-po 5574  df-so 5575

This theorem is used by:  soeq2  5596  wess  5652  wereu  5662  wereu2  5663  ordunifi  9260  fisup2g  9439  fisupcl  9440  fiinf2g  9472  ordtypelem8  9497  wemapso2lem  9524  iunfictbso  10117  fin1a2lem10  10411  fin1a2lem11  10412  zornn0g  10507  ltsopi  10891  npomex  10999  fimaxre  12177  fiminre  12180  suprfinzcl  12728  isercolllem1  15742  summolem2  15793  zsum  15795  prodmolem2  16015  zprod  16017  gsumval3  20008  iccpnfhmeo  25141  xrhmeo  25142  dvgt0lem2  26199  dgrval  26422  dgrcl  26427  dgrub  26428  dgrlb  26430  aannenlem3  26530  logccv  26865  nomaxmo  27899  nominmo  27900  n0fincut  28585  bdayfinbndlem1  28697  xrge0infssd  33143  infxrge0lb  33146  infxrge0glb  33147  infxrge0gelb  33148  ssnnssfz  33169  xrge0iifiso  34356  omsfval  34716  omsf  34718  oms0  34719  omssubaddlem  34721  omssubadd  34722  oddpwdc  34776  erdszelem4  35707  erdszelem8  35711  erdsze2lem1  35716  erdsze2lem2  35717  supfz  36242  inffz  36243  finorwe  38069  fin2so  38299  sticksstones3  42956  rencldnfilem  43588  fzisoeu  46060  fourierdlem36  46898  ssnn0ssfz  49170