Theorem wess 5624

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3914   Or wor 5545   Fr wfr 5588   We wwe 5590

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 3045  df-ss 3931  df-po 5546  df-so 5547  df-fr 5591  df-we 5593

This theorem is referenced by:  wefrc  5632  trssord  6349  ordelord  6354  dford5  7760  omsinds  7863  fnwelem  8110  dfrecs3  8341  ordtypelem8  9478  oismo  9493  cantnfcl  9620  infxpenlem  9966  ac10ct  9987  dfac12lem2  10098  cflim2  10216  cofsmo  10222  hsmexlem1  10379  smobeth  10539  canthwelem  10603  gruina  10771  ltwefz  13928  welb  37730  dnwech  43037  aomclem4  43046  dfac11  43051  oaun3lem1  43363  onfrALTlem3  44534  onfrALTlem3VD  44876