Theorem wess 5675

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3963   Or wor 5596   Fr wfr 5638   We wwe 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3060  df-ss 3980  df-po 5597  df-so 5598  df-fr 5641  df-we 5643

This theorem is referenced by:  wefrc  5683  trssord  6403  ordelord  6408  dford5  7803  omsinds  7908  omsindsOLD  7909  fnwelem  8155  wfrlem5OLD  8352  dfrecs3  8411  dfrecs3OLD  8412  ordtypelem8  9563  oismo  9578  cantnfcl  9705  infxpenlem  10051  ac10ct  10072  dfac12lem2  10183  cflim2  10301  cofsmo  10307  hsmexlem1  10464  smobeth  10624  canthwelem  10688  gruina  10856  ltwefz  14001  welb  37723  dnwech  43037  aomclem4  43046  dfac11  43051  oaun3lem1  43364  onfrALTlem3  44542  onfrALTlem3VD  44885