Theorem wess 5640

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 5618	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Fr 𝐵 → 𝑅 Fr 𝐴))
2		soss 5581	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))
3	1, 2	anim12d 609	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵) → (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)))
4		df-we 5608	. 2 ⊢ (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵))
5		df-we 5608	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
6	3, 4, 5	3imtr4g 296	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 We 𝐵 → 𝑅 We 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3926   Or wor 5560   Fr wfr 5603   We wwe 5605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3052  df-ss 3943  df-po 5561  df-so 5562  df-fr 5606  df-we 5608

This theorem is referenced by:  wefrc  5648  trssord  6369  ordelord  6374  dford5  7776  omsinds  7880  fnwelem  8128  wfrlem5OLD  8325  dfrecs3  8384  dfrecs3OLD  8385  ordtypelem8  9537  oismo  9552  cantnfcl  9679  infxpenlem  10025  ac10ct  10046  dfac12lem2  10157  cflim2  10275  cofsmo  10281  hsmexlem1  10438  smobeth  10598  canthwelem  10662  gruina  10830  ltwefz  13979  welb  37706  dnwech  43019  aomclem4  43028  dfac11  43033  oaun3lem1  43345  onfrALTlem3  44517  onfrALTlem3VD  44859