Theorem soss 5569

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085  ∀wral 3045   ⊆ wss 3917   class class class wbr 5110   Po wpo 5547   Or wor 5548

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 3046  df-ss 3934  df-po 5549  df-so 5550

This theorem is referenced by:  soeq2  5571  wess  5627  wereu  5637  wereu2  5638  ordunifi  9244  fisup2g  9427  fisupcl  9428  fiinf2g  9460  ordtypelem8  9485  wemapso2lem  9512  iunfictbso  10074  fin1a2lem10  10369  fin1a2lem11  10370  zornn0g  10465  ltsopi  10848  npomex  10956  fimaxre  12134  fiminre  12137  suprfinzcl  12655  isercolllem1  15638  summolem2  15689  zsum  15691  prodmolem2  15908  zprod  15910  gsumval3  19844  iccpnfhmeo  24850  xrhmeo  24851  dvgt0lem2  25915  dgrval  26140  dgrcl  26145  dgrub  26146  dgrlb  26148  aannenlem3  26245  logccv  26579  nomaxmo  27617  nominmo  27618  n0sfincut  28253  xrge0infssd  32691  infxrge0lb  32694  infxrge0glb  32695  infxrge0gelb  32696  ssnnssfz  32717  xrge0iifiso  33932  omsfval  34292  omsf  34294  oms0  34295  omssubaddlem  34297  omssubadd  34298  oddpwdc  34352  erdszelem4  35188  erdszelem8  35192  erdsze2lem1  35197  erdsze2lem2  35198  supfz  35723  inffz  35724  finorwe  37377  fin2so  37608  sticksstones3  42143  rencldnfilem  42815  fzisoeu  45305  fourierdlem36  46148  ssnn0ssfz  48341