Theorem soss 4977

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 4961	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴))
2		ssel 3562	. . . . . . 7 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3		ssel 3562	. . . . . . 7 ⊢ (𝐴 ⊆ 𝐵 → (𝑦 ∈ 𝐴 → 𝑦 ∈ 𝐵))
4	2, 3	anim12d 584	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)))
5	4	imim1d 80	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
6	5	2alimdv 1834	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥∀𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
7		r2al 2923	. . . 4 ⊢ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
8		r2al 2923	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) ↔ ∀𝑥∀𝑦((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
9	6, 7, 8	3imtr4g 284	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
10	1, 9	anim12d 584	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) → (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))))
11		df-so 4960	. 2 ⊢ (𝑅 Or 𝐵 ↔ (𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
12		df-so 4960	. 2 ⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)))
13	10, 11, 12	3imtr4g 284	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))

Syntax hints:   → wi 4   ∧ wa 383   ∨ w3o 1030  ∀wal 1473   ∈ wcel 1977  ∀wral 2896   ⊆ wss 3540   class class class wbr 4583   Po wpo 4957   Or wor 4958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-in 3547  df-ss 3554  df-po 4959  df-so 4960

This theorem is referenced by:  soeq2  4979  wess  5025  wereu  5034  wereu2  5035  ordunifi  8095  fisup2g  8257  fisupcl  8258  fiinf2g  8289  ordtypelem8  8313  wemapso2lem  8340  iunfictbso  8820  fin1a2lem10  9114  fin1a2lem11  9115  zornn0g  9210  ltsopi  9589  npomex  9697  fimaxre  10847  suprfinzcl  11368  isercolllem1  14243  summolem2  14294  zsum  14296  prodmolem2  14504  zprod  14506  gsumval3  18131  iccpnfhmeo  22552  xrhmeo  22553  dvgt0lem2  23570  dgrval  23788  dgrcl  23793  dgrub  23794  dgrlb  23796  aannenlem3  23889  logccv  24209  xrge0infssd  28916  infxrge0lb  28919  infxrge0glb  28920  infxrge0gelb  28921  ssnnssfz  28937  xrge0iifiso  29309  omsfval  29683  omsf  29685  oms0  29686  omssubaddlem  29688  omssubadd  29689  oddpwdc  29743  erdszelem4  30430  erdszelem8  30434  erdsze2lem1  30439  erdsze2lem2  30440  supfz  30866  inffz  30867  inffzOLD  30868  fin2so  32566  rencldnfilem  36402  fzisoeu  38455  fourierdlem36  39036  ssnn0ssfz  41920