Theorem soss 5573

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 5555	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
2		ss2ralv 4007	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3	1, 2	anim12d 618	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
4		df-so 5554	. 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5		df-so 5554	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
6	3, 4, 5	3imtr4g 298	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))

Syntax hints:   → wi 4   ∧ wa 399   ∨ w3o 1096  ∀wral 3075   ⊆ wss 3904   class class class wbr 5099   Po wpo 5551   Or wor 5552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ral 3076  df-ss 3921  df-po 5553  df-so 5554

This theorem is referenced by:  soeq2  5575  wess  5631  wereu  5641  wereu2  5642  ordunifi  9230  fisup2g  9412  fisupcl  9413  fiinf2g  9445  ordtypelem8  9470  wemapso2lem  9497  iunfictbso  10067  fin1a2lem10  10363  fin1a2lem11  10364  zornn0g  10459  ltsopi  10843  npomex  10951  fimaxre  12133  fiminre  12136  suprfinzcl  12684  isercolllem1  15675  summolem2  15726  zsum  15728  prodmolem2  15948  zprod  15950  gsumval3  19930  iccpnfhmeo  24987  xrhmeo  24988  dvgt0lem2  26045  dgrval  26268  dgrcl  26273  dgrub  26274  dgrlb  26276  aannenlem3  26371  logccv  26705  nomaxmo  27739  nominmo  27740  n0fincut  28425  bdayfinbndlem1  28537  xrge0infssd  32913  infxrge0lb  32916  infxrge0glb  32917  infxrge0gelb  32918  ssnnssfz  32939  xrge0iifiso  34193  omsfval  34552  omsf  34554  oms0  34555  omssubaddlem  34557  omssubadd  34558  oddpwdc  34612  erdszelem4  35508  erdszelem8  35512  erdsze2lem1  35517  erdsze2lem2  35518  supfz  36043  inffz  36044  finorwe  37840  fin2so  38070  sticksstones3  42729  rencldnfilem  43361  fzisoeu  45843  fourierdlem36  46681  ssnn0ssfz  48935