Theorem soss 5544

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1085  ∀wral 3047   ⊆ wss 3902   class class class wbr 5091   Po wpo 5522   Or wor 5523

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3048  df-ss 3919  df-po 5524  df-so 5525

This theorem is referenced by:  soeq2  5546  wess  5602  wereu  5612  wereu2  5613  ordunifi  9174  fisup2g  9353  fisupcl  9354  fiinf2g  9386  ordtypelem8  9411  wemapso2lem  9438  iunfictbso  10002  fin1a2lem10  10297  fin1a2lem11  10298  zornn0g  10393  ltsopi  10776  npomex  10884  fimaxre  12063  fiminre  12066  suprfinzcl  12584  isercolllem1  15569  summolem2  15620  zsum  15622  prodmolem2  15839  zprod  15841  gsumval3  19817  iccpnfhmeo  24868  xrhmeo  24869  dvgt0lem2  25933  dgrval  26158  dgrcl  26163  dgrub  26164  dgrlb  26166  aannenlem3  26263  logccv  26597  nomaxmo  27635  nominmo  27636  n0sfincut  28280  xrge0infssd  32739  infxrge0lb  32742  infxrge0glb  32743  infxrge0gelb  32744  ssnnssfz  32765  xrge0iifiso  33943  omsfval  34302  omsf  34304  oms0  34305  omssubaddlem  34307  omssubadd  34308  oddpwdc  34362  erdszelem4  35226  erdszelem8  35230  erdsze2lem1  35235  erdsze2lem2  35236  supfz  35761  inffz  35762  finorwe  37415  fin2so  37646  sticksstones3  42180  rencldnfilem  42852  fzisoeu  45340  fourierdlem36  46180  ssnn0ssfz  48379