Theorem soss 5612

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1086  ∀wral 3061   ⊆ wss 3951   class class class wbr 5143   Po wpo 5590   Or wor 5591

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 3062  df-ss 3968  df-po 5592  df-so 5593

This theorem is referenced by:  soeq2  5614  wess  5671  wereu  5681  wereu2  5682  ordunifi  9326  fisup2g  9508  fisupcl  9509  fiinf2g  9540  ordtypelem8  9565  wemapso2lem  9592  iunfictbso  10154  fin1a2lem10  10449  fin1a2lem11  10450  zornn0g  10545  ltsopi  10928  npomex  11036  fimaxre  12212  fiminre  12215  suprfinzcl  12732  isercolllem1  15701  summolem2  15752  zsum  15754  prodmolem2  15971  zprod  15973  gsumval3  19925  iccpnfhmeo  24976  xrhmeo  24977  dvgt0lem2  26042  dgrval  26267  dgrcl  26272  dgrub  26273  dgrlb  26275  aannenlem3  26372  logccv  26705  nomaxmo  27743  nominmo  27744  xrge0infssd  32765  infxrge0lb  32768  infxrge0glb  32769  infxrge0gelb  32770  ssnnssfz  32789  xrge0iifiso  33934  omsfval  34296  omsf  34298  oms0  34299  omssubaddlem  34301  omssubadd  34302  oddpwdc  34356  erdszelem4  35199  erdszelem8  35203  erdsze2lem1  35208  erdsze2lem2  35209  supfz  35729  inffz  35730  finorwe  37383  fin2so  37614  sticksstones3  42149  rencldnfilem  42831  fzisoeu  45312  fourierdlem36  46158  ssnn0ssfz  48265