Theorem wess 5686

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

Assertion

Ref	Expression
wess	⊢ (𝐴 ⊆ 𝐵 → (𝑅 We 𝐵 → 𝑅 We 𝐴))

Proof of Theorem wess

Step	Hyp	Ref	Expression
1		frss 5664	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Fr 𝐵 → 𝑅 Fr 𝐴))
2		soss 5628	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))
3	1, 2	anim12d 608	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵) → (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)))
4		df-we 5654	. 2 ⊢ (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵))
5		df-we 5654	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
6	3, 4, 5	3imtr4g 296	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 We 𝐵 → 𝑅 We 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3976   Or wor 5606   Fr wfr 5649   We wwe 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3068  df-ss 3993  df-po 5607  df-so 5608  df-fr 5652  df-we 5654

This theorem is referenced by:  wefrc  5694  trssord  6412  ordelord  6417  dford5  7819  omsinds  7924  omsindsOLD  7925  fnwelem  8172  wfrlem5OLD  8369  dfrecs3  8428  dfrecs3OLD  8429  ordtypelem8  9594  oismo  9609  cantnfcl  9736  infxpenlem  10082  ac10ct  10103  dfac12lem2  10214  cflim2  10332  cofsmo  10338  hsmexlem1  10495  smobeth  10655  canthwelem  10719  gruina  10887  ltwefz  14014  welb  37696  dnwech  43005  aomclem4  43014  dfac11  43019  oaun3lem1  43336  onfrALTlem3  44515  onfrALTlem3VD  44858