Theorem soss 5580

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 5562	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
2		ss2ralv 4010	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
3	1, 2	anim12d 620	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
4		df-so 5561	. 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
5		df-so 5561	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
6	3, 4, 5	3imtr4g 299	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))

Syntax hints:   → wi 4   ∧ wa 400   ∨ w3o 1100  ∀wral 3079   ⊆ wss 3907   class class class wbr 5105   Po wpo 5558   Or wor 5559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3080  df-ss 3924  df-po 5560  df-so 5561

This theorem is referenced by:  soeq2  5582  wess  5638  wereu  5648  wereu2  5649  ordunifi  9238  fisup2g  9417  fisupcl  9418  fiinf2g  9450  ordtypelem8  9475  wemapso2lem  9502  iunfictbso  10086  fin1a2lem10  10381  fin1a2lem11  10382  zornn0g  10477  ltsopi  10861  npomex  10969  fimaxre  12150  fiminre  12153  suprfinzcl  12701  isercolllem1  15706  summolem2  15757  zsum  15759  prodmolem2  15979  zprod  15981  gsumval3  19968  iccpnfhmeo  25065  xrhmeo  25066  dvgt0lem2  26123  dgrval  26346  dgrcl  26351  dgrub  26352  dgrlb  26354  aannenlem3  26452  logccv  26786  nomaxmo  27820  nominmo  27821  n0fincut  28506  bdayfinbndlem1  28618  xrge0infssd  33018  infxrge0lb  33021  infxrge0glb  33022  infxrge0gelb  33023  ssnnssfz  33044  xrge0iifiso  34242  omsfval  34601  omsf  34603  oms0  34604  omssubaddlem  34606  omssubadd  34607  oddpwdc  34661  erdszelem4  35557  erdszelem8  35561  erdsze2lem1  35566  erdsze2lem2  35567  supfz  36092  inffz  36093  finorwe  37888  fin2so  38118  sticksstones3  42777  rencldnfilem  43409  fzisoeu  45877  fourierdlem36  46715  ssnn0ssfz  48980