Theorem soss 5583

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ w3o 1102  ∀wral 3080   ⊆ wss 3900   class class class wbr 5106   Po wpo 5561   Or wor 5562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3081  df-ss 3901  df-po 5563  df-so 5564

This theorem is used by:  soeq2  5585  wess  5641  wereu  5651  wereu2  5652  ordunifi  9309  fisup2g  9488  fisupcl  9489  fiinf2g  9521  ordtypelem8  9546  wemapso2lem  9573  iunfictbso  10220  fin1a2lem10  10514  fin1a2lem11  10515  zornn0g  10610  ltsopi  11000  npomex  11108  fimaxre  12288  fiminre  12291  suprfinzcl  12840  isercolllem1  15861  summolem2  15911  zsum  15913  prodmolem2  16131  zprod  16133  gsumval3  20151  iccpnfhmeo  25296  xrhmeo  25297  dvgt0lem2  26353  dgrval  26577  dgrcl  26582  dgrub  26583  dgrlb  26585  aannenlem3  26687  logccv  27021  nomaxmo  28085  nominmo  28086  n0fincut  28771  bdayfinbndlem1  28883  xrge0infssd  33423  infxrge0lb  33426  infxrge0glb  33427  infxrge0gelb  33428  ssnnssfz  33449  xrge0iifiso  34637  omsfval  34996  omsf  34998  oms0  34999  omssubaddlem  35001  omssubadd  35002  oddpwdc  35056  erdszelem4  36126  erdszelem8  36130  erdsze2lem1  36135  erdsze2lem2  36136  supfz  36672  inffz  36673  finorwe  38497  fin2so  38722  sticksstones3  43390  rencldnfilem  44020  fzisoeu  46521  fourierdlem36  47358  ssnn0ssfz  49666