Theorem soss 5578

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 5560	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
2		ss2ralv 3979	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3	1, 2	anim12d 621	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
4		df-so 5559	. 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5		df-so 5559	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
6	3, 4, 5	3imtr4g 299	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ w3o 1102  ∀wral 3076   ⊆ wss 3895   class class class wbr 5102   Po wpo 5556   Or wor 5557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077  df-ss 3896  df-po 5558  df-so 5559

This theorem is used by:  soeq2  5580  wess  5636  wereu  5646  wereu2  5647  ordunifi  9284  fisup2g  9464  fisupcl  9465  fiinf2g  9497  ordtypelem8  9522  wemapso2lem  9549  iunfictbso  10196  fin1a2lem10  10490  fin1a2lem11  10491  zornn0g  10586  ltsopi  10976  npomex  11084  fimaxre  12264  fiminre  12267  suprfinzcl  12816  isercolllem1  15837  summolem2  15887  zsum  15889  prodmolem2  16107  zprod  16109  gsumval3  20126  iccpnfhmeo  25271  xrhmeo  25272  dvgt0lem2  26328  dgrval  26552  dgrcl  26557  dgrub  26558  dgrlb  26560  aannenlem3  26662  logccv  26996  nomaxmo  28060  nominmo  28061  n0fincut  28746  bdayfinbndlem1  28858  xrge0infssd  33399  infxrge0lb  33402  infxrge0glb  33403  infxrge0gelb  33404  ssnnssfz  33425  xrge0iifiso  34613  omsfval  34972  omsf  34974  oms0  34975  omssubaddlem  34977  omssubadd  34978  oddpwdc  35032  erdszelem4  36045  erdszelem8  36049  erdsze2lem1  36054  erdsze2lem2  36055  supfz  36586  inffz  36587  finorwe  38398  fin2so  38623  sticksstones3  43291  rencldnfilem  43920  fzisoeu  46409  fourierdlem36  47246  ssnn0ssfz  49554