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  9281  fisup2g  9461  fisupcl  9462  fiinf2g  9494  ordtypelem8  9519  wemapso2lem  9546  iunfictbso  10193  fin1a2lem10  10487  fin1a2lem11  10488  zornn0g  10583  ltsopi  10973  npomex  11081  fimaxre  12261  fiminre  12264  suprfinzcl  12813  isercolllem1  15832  summolem2  15882  zsum  15884  prodmolem2  16102  zprod  16104  gsumval3  20121  iccpnfhmeo  25266  xrhmeo  25267  dvgt0lem2  26323  dgrval  26547  dgrcl  26552  dgrub  26553  dgrlb  26555  aannenlem3  26657  logccv  26991  nomaxmo  28055  nominmo  28056  n0fincut  28741  bdayfinbndlem1  28853  xrge0infssd  33395  infxrge0lb  33398  infxrge0glb  33399  infxrge0gelb  33400  ssnnssfz  33421  xrge0iifiso  34609  omsfval  34968  omsf  34970  oms0  34971  omssubaddlem  34973  omssubadd  34974  oddpwdc  35028  erdszelem4  36001  erdszelem8  36005  erdsze2lem1  36010  erdsze2lem2  36011  supfz  36536  inffz  36537  finorwe  38348  fin2so  38573  sticksstones3  43241  rencldnfilem  43870  fzisoeu  46359  fourierdlem36  47196  ssnn0ssfz  49504