Theorem wess 5626

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 5604	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Fr 𝐵 → 𝑅 Fr 𝐴))
2		soss 5568	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))
3	1, 2	anim12d 617	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵) → (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)))
4		df-we 5595	. 2 ⊢ (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵))
5		df-we 5595	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
6	3, 4, 5	3imtr4g 298	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 We 𝐵 → 𝑅 We 𝐴))

Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3899   Or wor 5547   Fr wfr 5590   We wwe 5592

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ral 3071  df-ss 3916  df-po 5548  df-so 5549  df-fr 5593  df-we 5595

This theorem is referenced by:  wefrc  5634  trssord  6352  ordelord  6357  dford5  7756  omsinds  7856  fnwelem  8099  dfrecs3  8331  ordtypelem8  9463  oismo  9478  cantnfcl  9612  infxpenlem  9959  ac10ct  9980  dfac12lem2  10091  cflim2  10210  cofsmo  10216  hsmexlem1  10373  smobeth  10534  canthwelem  10598  gruina  10766  ltwefz  13966  welb  38183  dnwech  43573  aomclem4  43582  dfac11  43587  oaun3lem1  43899  onfrALTlem3  45068  onfrALTlem3VD  45410