Theorem soss 5581

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085  ∀wral 3051   ⊆ wss 3926   class class class wbr 5119   Po wpo 5559   Or wor 5560

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 3052  df-ss 3943  df-po 5561  df-so 5562

This theorem is referenced by:  soeq2  5583  wess  5640  wereu  5650  wereu2  5651  ordunifi  9298  fisup2g  9481  fisupcl  9482  fiinf2g  9514  ordtypelem8  9539  wemapso2lem  9566  iunfictbso  10128  fin1a2lem10  10423  fin1a2lem11  10424  zornn0g  10519  ltsopi  10902  npomex  11010  fimaxre  12186  fiminre  12189  suprfinzcl  12707  isercolllem1  15681  summolem2  15732  zsum  15734  prodmolem2  15951  zprod  15953  gsumval3  19888  iccpnfhmeo  24894  xrhmeo  24895  dvgt0lem2  25960  dgrval  26185  dgrcl  26190  dgrub  26191  dgrlb  26193  aannenlem3  26290  logccv  26624  nomaxmo  27662  nominmo  27663  n0sfincut  28298  xrge0infssd  32738  infxrge0lb  32741  infxrge0glb  32742  infxrge0gelb  32743  ssnnssfz  32764  xrge0iifiso  33966  omsfval  34326  omsf  34328  oms0  34329  omssubaddlem  34331  omssubadd  34332  oddpwdc  34386  erdszelem4  35216  erdszelem8  35220  erdsze2lem1  35225  erdsze2lem2  35226  supfz  35746  inffz  35747  finorwe  37400  fin2so  37631  sticksstones3  42161  rencldnfilem  42843  fzisoeu  45329  fourierdlem36  46172  ssnn0ssfz  48324