Theorem wess 4871

Description: Subset theorem for the well-ordering predicate. Exercise 4 of [TakeutiZaring] p. 31. (Contributed by NM, 19-Apr-1994.)

Assertion

Ref	Expression
wess

Proof of Theorem wess

Step	Hyp	Ref	Expression
1		frss 4851	. . 3
2		soss 4823	. . 3
3	1, 2	anim12d 563	. 2
4		df-we 4845	. 2
5		df-we 4845	. 2
6	3, 4, 5	3imtr4g 270	1

Syntax hints:  ->wi 4  /\wa 369  C_wss 3475  Orwor 4804  Frwfr 4840  Wewwe 4842

This theorem is referenced by:  wefrc  4878  trssord  4900  ordelord  4905  fnwelem  6915  ordtypelem8  7971  oismo  7986  cantnfcl  8107  cantnfclOLD  8137  infxpenlem  8412  ac10ct  8436  dfac12lem2  8545  cflim2  8664  cofsmo  8670  hsmexlem1  8827  smobeth  8982  canthwelem  9049  gruina  9217  ltwefz  12074  omsinds  29299  wfrlem5  29347  welb  30227  dnwech  30994  aomclem4  31003  dfac11  31008  onfrALTlem3  33316  onfrALTlem3VD  33687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-in 3482  df-ss 3489  df-po 4805  df-so 4806  df-fr 4843  df-we 4845