Theorem soss 5605

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ w3o 1084  ∀wral 3057   ⊆ wss 3945   class class class wbr 5143   Po wpo 5583   Or wor 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3058  df-v 3472  df-in 3952  df-ss 3962  df-po 5585  df-so 5586

This theorem is referenced by:  soeq2  5607  wess  5660  wereu  5669  wereu2  5670  ordunifi  9312  fisup2g  9486  fisupcl  9487  fiinf2g  9518  ordtypelem8  9543  wemapso2lem  9570  iunfictbso  10132  fin1a2lem10  10427  fin1a2lem11  10428  zornn0g  10523  ltsopi  10906  npomex  11014  fimaxre  12183  fiminre  12186  suprfinzcl  12701  isercolllem1  15638  summolem2  15689  zsum  15691  prodmolem2  15906  zprod  15908  gsumval3  19856  iccpnfhmeo  24864  xrhmeo  24865  dvgt0lem2  25930  dgrval  26156  dgrcl  26161  dgrub  26162  dgrlb  26164  aannenlem3  26259  logccv  26591  nomaxmo  27625  nominmo  27626  xrge0infssd  32526  infxrge0lb  32529  infxrge0glb  32530  infxrge0gelb  32531  ssnnssfz  32550  xrge0iifiso  33531  omsfval  33909  omsf  33911  oms0  33912  omssubaddlem  33914  omssubadd  33915  oddpwdc  33969  erdszelem4  34799  erdszelem8  34803  erdsze2lem1  34808  erdsze2lem2  34809  supfz  35318  inffz  35319  finorwe  36856  fin2so  37075  sticksstones3  41615  rencldnfilem  42231  fzisoeu  44673  fourierdlem36  45522  ssnn0ssfz  47404