Theorem soss 5591

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

Syntax hints:   → wi 4   ∧ wa 400   ∨ w3o 1102  ∀wral 3079   ⊆ wss 3906   class class class wbr 5110   Po wpo 5569   Or wor 5570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3080  df-ss 3923  df-po 5571  df-so 5572

This theorem is referenced by:  soeq2  5593  wess  5649  wereu  5659  wereu2  5660  ordunifi  9251  fisup2g  9430  fisupcl  9431  fiinf2g  9463  ordtypelem8  9488  wemapso2lem  9515  iunfictbso  10099  fin1a2lem10  10394  fin1a2lem11  10395  zornn0g  10490  ltsopi  10874  npomex  10982  fimaxre  12160  fiminre  12163  suprfinzcl  12711  isercolllem1  15718  summolem2  15769  zsum  15771  prodmolem2  15991  zprod  15993  gsumval3  19978  iccpnfhmeo  25085  xrhmeo  25086  dvgt0lem2  26143  dgrval  26366  dgrcl  26371  dgrub  26372  dgrlb  26374  aannenlem3  26472  logccv  26806  nomaxmo  27840  nominmo  27841  n0fincut  28526  bdayfinbndlem1  28638  xrge0infssd  33084  infxrge0lb  33087  infxrge0glb  33088  infxrge0gelb  33089  ssnnssfz  33110  xrge0iifiso  34303  omsfval  34662  omsf  34664  oms0  34665  omssubaddlem  34667  omssubadd  34668  oddpwdc  34722  erdszelem4  35664  erdszelem8  35668  erdsze2lem1  35673  erdsze2lem2  35674  supfz  36199  inffz  36200  finorwe  38006  fin2so  38236  sticksstones3  42893  rencldnfilem  43527  fzisoeu  45999  fourierdlem36  46837  ssnn0ssfz  49106