Theorem wess 5618

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3903   Or wor 5539   Fr wfr 5582   We wwe 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053  df-ss 3920  df-po 5540  df-so 5541  df-fr 5585  df-we 5587

This theorem is referenced by:  wefrc  5626  trssord  6342  ordelord  6347  dford5  7739  omsinds  7839  fnwelem  8083  dfrecs3  8314  ordtypelem8  9442  oismo  9457  cantnfcl  9588  infxpenlem  9935  ac10ct  9956  dfac12lem2  10067  cflim2  10185  cofsmo  10191  hsmexlem1  10348  smobeth  10509  canthwelem  10573  gruina  10741  ltwefz  13898  welb  37976  dnwech  43394  aomclem4  43403  dfac11  43408  oaun3lem1  43720  onfrALTlem3  44889  onfrALTlem3VD  45231