Theorem wess 5641

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 5619	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Fr 𝐵 → 𝑅 Fr 𝐴))
2		soss 5583	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))
3	1, 2	anim12d 621	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵) → (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)))
4		df-we 5610	. 2 ⊢ (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵))
5		df-we 5610	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
6	3, 4, 5	3imtr4g 299	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 We 𝐵 → 𝑅 We 𝐴))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3900   Or wor 5562   Fr wfr 5605   We wwe 5607

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3081  df-ss 3901  df-po 5563  df-so 5564  df-fr 5608  df-we 5610

This theorem is used by:  wefrc  5649  trssord  6397  ordelord  6402  f1we  7386  dford5  7822  omsinds  7922  fnwelem  8170  dfrecs3  8408  ordtypelem8  9546  oismo  9561  cantnfcl  9695  infxpenlem  10119  ac10ct  10140  dfac12lem2  10250  cflim2  10368  cofsmo  10374  hsmexlem1  10531  smobeth  10698  canthwelem  10762  gruina  10930  ltwefz  14133  onf1we  35803  wevsev  36041  wevonprcf1o  36042  vonf1onprcf1ac  36044  onprcf1acwevdlem1  36045  onprcf1acwevdlem2  36046  onprcr  36631  welb  38862  aomclem4  44252  dfac11  44257  oaun3lem1  44568  onfrALTlem3  45718  onfrALTlem3VD  46060