Theorem soss 5559

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1086  ∀wral 3051   ⊆ wss 3889   class class class wbr 5085   Po wpo 5537   Or wor 5538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3052  df-ss 3906  df-po 5539  df-so 5540

This theorem is referenced by:  soeq2  5561  wess  5617  wereu  5627  wereu2  5628  ordunifi  9200  fisup2g  9382  fisupcl  9383  fiinf2g  9415  ordtypelem8  9440  wemapso2lem  9467  iunfictbso  10036  fin1a2lem10  10331  fin1a2lem11  10332  zornn0g  10427  ltsopi  10811  npomex  10919  fimaxre  12100  fiminre  12103  suprfinzcl  12643  isercolllem1  15627  summolem2  15678  zsum  15680  prodmolem2  15900  zprod  15902  gsumval3  19882  iccpnfhmeo  24912  xrhmeo  24913  dvgt0lem2  25970  dgrval  26193  dgrcl  26198  dgrub  26199  dgrlb  26201  aannenlem3  26296  logccv  26627  nomaxmo  27662  nominmo  27663  n0fincut  28347  bdayfinbndlem1  28459  xrge0infssd  32834  infxrge0lb  32837  infxrge0glb  32838  infxrge0gelb  32839  ssnnssfz  32860  xrge0iifiso  34079  omsfval  34438  omsf  34440  oms0  34441  omssubaddlem  34443  omssubadd  34444  oddpwdc  34498  erdszelem4  35376  erdszelem8  35380  erdsze2lem1  35385  erdsze2lem2  35386  supfz  35911  inffz  35912  finorwe  37698  fin2so  37928  sticksstones3  42587  rencldnfilem  43248  fzisoeu  45733  fourierdlem36  46571  ssnn0ssfz  48825