Theorem wess 5607

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3899   Or wor 5528   Fr wfr 5571   We wwe 5573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3050  df-ss 3916  df-po 5529  df-so 5530  df-fr 5574  df-we 5576

This theorem is referenced by:  wefrc  5615  trssord  6331  ordelord  6336  dford5  7726  omsinds  7826  fnwelem  8070  dfrecs3  8301  ordtypelem8  9421  oismo  9436  cantnfcl  9567  infxpenlem  9914  ac10ct  9935  dfac12lem2  10046  cflim2  10164  cofsmo  10170  hsmexlem1  10327  smobeth  10487  canthwelem  10551  gruina  10719  ltwefz  13880  welb  37786  dnwech  43155  aomclem4  43164  dfac11  43169  oaun3lem1  43481  onfrALTlem3  44651  onfrALTlem3VD  44993