Theorem soss 5495

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 5478	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
2		ss2ralv 4037	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3	1, 2	anim12d 610	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
4		df-so 5477	. 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5		df-so 5477	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
6	3, 4, 5	3imtr4g 298	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))

Syntax hints:   → wi 4   ∧ wa 398   ∨ w3o 1082  ∀wral 3140   ⊆ wss 3938   class class class wbr 5068   Po wpo 5474   Or wor 5475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ral 3145  df-in 3945  df-ss 3954  df-po 5476  df-so 5477

This theorem is referenced by:  soeq2  5497  wess  5544  wereu  5553  wereu2  5554  ordunifi  8770  fisup2g  8934  fisupcl  8935  fiinf2g  8966  ordtypelem8  8991  wemapso2lem  9018  iunfictbso  9542  fin1a2lem10  9833  fin1a2lem11  9834  zornn0g  9929  ltsopi  10312  npomex  10420  fimaxre  11586  fimaxreOLD  11587  fiminre  11590  suprfinzcl  12100  isercolllem1  15023  summolem2  15075  zsum  15077  prodmolem2  15291  zprod  15293  gsumval3  19029  iccpnfhmeo  23551  xrhmeo  23552  dvgt0lem2  24602  dgrval  24820  dgrcl  24825  dgrub  24826  dgrlb  24828  aannenlem3  24921  logccv  25248  xrge0infssd  30487  infxrge0lb  30490  infxrge0glb  30491  infxrge0gelb  30492  ssnnssfz  30512  xrge0iifiso  31180  omsfval  31554  omsf  31556  oms0  31557  omssubaddlem  31559  omssubadd  31560  oddpwdc  31614  erdszelem4  32443  erdszelem8  32447  erdsze2lem1  32452  erdsze2lem2  32453  supfz  32962  inffz  32963  nomaxmo  33203  finorwe  34665  fin2so  34881  rencldnfilem  39424  fzisoeu  41574  fourierdlem36  42435  ssnn0ssfz  44404