Theorem soss 5592

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085  ∀wral 3050   ⊆ wss 3931   class class class wbr 5123   Po wpo 5570   Or wor 5571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3051  df-ss 3948  df-po 5572  df-so 5573

This theorem is referenced by:  soeq2  5594  wess  5651  wereu  5661  wereu2  5662  ordunifi  9308  fisup2g  9490  fisupcl  9491  fiinf2g  9522  ordtypelem8  9547  wemapso2lem  9574  iunfictbso  10136  fin1a2lem10  10431  fin1a2lem11  10432  zornn0g  10527  ltsopi  10910  npomex  11018  fimaxre  12194  fiminre  12197  suprfinzcl  12715  isercolllem1  15684  summolem2  15735  zsum  15737  prodmolem2  15954  zprod  15956  gsumval3  19894  iccpnfhmeo  24913  xrhmeo  24914  dvgt0lem2  25979  dgrval  26204  dgrcl  26209  dgrub  26210  dgrlb  26212  aannenlem3  26309  logccv  26642  nomaxmo  27680  nominmo  27681  xrge0infssd  32707  infxrge0lb  32710  infxrge0glb  32711  infxrge0gelb  32712  ssnnssfz  32733  xrge0iifiso  33909  omsfval  34271  omsf  34273  oms0  34274  omssubaddlem  34276  omssubadd  34277  oddpwdc  34331  erdszelem4  35174  erdszelem8  35178  erdsze2lem1  35183  erdsze2lem2  35184  supfz  35704  inffz  35705  finorwe  37358  fin2so  37589  sticksstones3  42124  rencldnfilem  42809  fzisoeu  45284  fourierdlem36  46130  ssnn0ssfz  48238