Theorem soss 5616

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085  ∀wral 3058   ⊆ wss 3962   class class class wbr 5147   Po wpo 5594   Or wor 5595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3059  df-ss 3979  df-po 5596  df-so 5597

This theorem is referenced by:  soeq2  5618  wess  5674  wereu  5684  wereu2  5685  ordunifi  9323  fisup2g  9505  fisupcl  9506  fiinf2g  9537  ordtypelem8  9562  wemapso2lem  9589  iunfictbso  10151  fin1a2lem10  10446  fin1a2lem11  10447  zornn0g  10542  ltsopi  10925  npomex  11033  fimaxre  12209  fiminre  12212  suprfinzcl  12729  isercolllem1  15697  summolem2  15748  zsum  15750  prodmolem2  15967  zprod  15969  gsumval3  19939  iccpnfhmeo  24989  xrhmeo  24990  dvgt0lem2  26056  dgrval  26281  dgrcl  26286  dgrub  26287  dgrlb  26289  aannenlem3  26386  logccv  26719  nomaxmo  27757  nominmo  27758  xrge0infssd  32771  infxrge0lb  32774  infxrge0glb  32775  infxrge0gelb  32776  ssnnssfz  32795  xrge0iifiso  33895  omsfval  34275  omsf  34277  oms0  34278  omssubaddlem  34280  omssubadd  34281  oddpwdc  34335  erdszelem4  35178  erdszelem8  35182  erdsze2lem1  35187  erdsze2lem2  35188  supfz  35708  inffz  35709  finorwe  37364  fin2so  37593  sticksstones3  42129  rencldnfilem  42807  fzisoeu  45250  fourierdlem36  46098  ssnn0ssfz  48193