Theorem soss 5523

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ w3o 1085  ∀wral 3064   ⊆ wss 3887   class class class wbr 5074   Po wpo 5501   Or wor 5502

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-v 3434  df-in 3894  df-ss 3904  df-po 5503  df-so 5504

This theorem is referenced by:  soeq2  5525  wess  5576  wereu  5585  wereu2  5586  ordunifi  9064  fisup2g  9227  fisupcl  9228  fiinf2g  9259  ordtypelem8  9284  wemapso2lem  9311  iunfictbso  9870  fin1a2lem10  10165  fin1a2lem11  10166  zornn0g  10261  ltsopi  10644  npomex  10752  fimaxre  11919  fiminre  11922  suprfinzcl  12436  isercolllem1  15376  summolem2  15428  zsum  15430  prodmolem2  15645  zprod  15647  gsumval3  19508  iccpnfhmeo  24108  xrhmeo  24109  dvgt0lem2  25167  dgrval  25389  dgrcl  25394  dgrub  25395  dgrlb  25397  aannenlem3  25490  logccv  25818  xrge0infssd  31084  infxrge0lb  31087  infxrge0glb  31088  infxrge0gelb  31089  ssnnssfz  31108  xrge0iifiso  31885  omsfval  32261  omsf  32263  oms0  32264  omssubaddlem  32266  omssubadd  32267  oddpwdc  32321  erdszelem4  33156  erdszelem8  33160  erdsze2lem1  33165  erdsze2lem2  33166  supfz  33694  inffz  33695  nomaxmo  33901  nominmo  33902  finorwe  35553  fin2so  35764  sticksstones3  40104  rencldnfilem  40642  fzisoeu  42839  fourierdlem36  43684  ssnn0ssfz  45685