Theorem soss 5553

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ w3o 1091  ∀wral 3054   ⊆ wss 3890   class class class wbr 5079   Po wpo 5531   Or wor 5532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3055  df-ss 3907  df-po 5533  df-so 5534

This theorem is referenced by:  soeq2  5555  wess  5611  wereu  5621  wereu2  5622  ordunifi  9197  fisup2g  9379  fisupcl  9380  fiinf2g  9412  ordtypelem8  9437  wemapso2lem  9464  iunfictbso  10034  fin1a2lem10  10329  fin1a2lem11  10330  zornn0g  10425  ltsopi  10809  npomex  10917  fimaxre  12098  fiminre  12101  suprfinzcl  12641  isercolllem1  15625  summolem2  15676  zsum  15678  prodmolem2  15898  zprod  15900  gsumval3  19880  iccpnfhmeo  24937  xrhmeo  24938  dvgt0lem2  25995  dgrval  26218  dgrcl  26223  dgrub  26224  dgrlb  26226  aannenlem3  26321  logccv  26652  nomaxmo  27687  nominmo  27688  n0fincut  28372  bdayfinbndlem1  28484  xrge0infssd  32860  infxrge0lb  32863  infxrge0glb  32864  infxrge0gelb  32865  ssnnssfz  32886  xrge0iifiso  34126  omsfval  34485  omsf  34487  oms0  34488  omssubaddlem  34490  omssubadd  34491  oddpwdc  34545  erdszelem4  35429  erdszelem8  35433  erdsze2lem1  35438  erdsze2lem2  35439  supfz  35964  inffz  35965  finorwe  37751  fin2so  37981  sticksstones3  42640  rencldnfilem  43272  fzisoeu  45755  fourierdlem36  46593  ssnn0ssfz  48847