Theorem soss 5609

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

Syntax hints:   → wi 4   ∧ wa 397   ∨ w3o 1087  ∀wral 3062   ⊆ wss 3949   class class class wbr 5149   Po wpo 5587   Or wor 5588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-v 3477  df-in 3956  df-ss 3966  df-po 5589  df-so 5590

This theorem is referenced by:  soeq2  5611  wess  5664  wereu  5673  wereu2  5674  ordunifi  9293  fisup2g  9463  fisupcl  9464  fiinf2g  9495  ordtypelem8  9520  wemapso2lem  9547  iunfictbso  10109  fin1a2lem10  10404  fin1a2lem11  10405  zornn0g  10500  ltsopi  10883  npomex  10991  fimaxre  12158  fiminre  12161  suprfinzcl  12676  isercolllem1  15611  summolem2  15662  zsum  15664  prodmolem2  15879  zprod  15881  gsumval3  19775  iccpnfhmeo  24461  xrhmeo  24462  dvgt0lem2  25520  dgrval  25742  dgrcl  25747  dgrub  25748  dgrlb  25750  aannenlem3  25843  logccv  26171  nomaxmo  27201  nominmo  27202  xrge0infssd  31974  infxrge0lb  31977  infxrge0glb  31978  infxrge0gelb  31979  ssnnssfz  31998  xrge0iifiso  32915  omsfval  33293  omsf  33295  oms0  33296  omssubaddlem  33298  omssubadd  33299  oddpwdc  33353  erdszelem4  34185  erdszelem8  34189  erdsze2lem1  34194  erdsze2lem2  34195  supfz  34698  inffz  34699  finorwe  36263  fin2so  36475  sticksstones3  40964  rencldnfilem  41558  fzisoeu  44010  fourierdlem36  44859  ssnn0ssfz  47025