Theorem soss 5579

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 5561	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
2		ss2ralv 4002	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3	1, 2	anim12d 621	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
4		df-so 5560	. 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5		df-so 5560	. 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 3077   ⊆ wss 3899   class class class wbr 5103   Po wpo 5557   Or wor 5558

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3078  df-ss 3916  df-po 5559  df-so 5560

This theorem is used by:  soeq2  5581  wess  5637  wereu  5647  wereu2  5648  ordunifi  9265  fisup2g  9445  fisupcl  9446  fiinf2g  9478  ordtypelem8  9503  wemapso2lem  9530  iunfictbso  10174  fin1a2lem10  10468  fin1a2lem11  10469  zornn0g  10564  ltsopi  10954  npomex  11062  fimaxre  12242  fiminre  12245  suprfinzcl  12794  isercolllem1  15812  summolem2  15862  zsum  15864  prodmolem2  16082  zprod  16084  gsumval3  20101  iccpnfhmeo  25246  xrhmeo  25247  dvgt0lem2  26303  dgrval  26527  dgrcl  26532  dgrub  26533  dgrlb  26535  aannenlem3  26639  logccv  26973  nomaxmo  28037  nominmo  28038  n0fincut  28723  bdayfinbndlem1  28835  xrge0infssd  33335  infxrge0lb  33338  infxrge0glb  33339  infxrge0gelb  33340  ssnnssfz  33361  xrge0iifiso  34549  omsfval  34909  omsf  34911  oms0  34912  omssubaddlem  34914  omssubadd  34915  oddpwdc  34969  erdszelem4  35928  erdszelem8  35932  erdsze2lem1  35937  erdsze2lem2  35938  supfz  36463  inffz  36464  finorwe  38273  fin2so  38498  sticksstones3  43166  rencldnfilem  43780  fzisoeu  46259  fourierdlem36  47097  ssnn0ssfz  49405