Theorem wess 5609

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3905   Or wor 5530   Fr wfr 5573   We wwe 5575

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3045  df-ss 3922  df-po 5531  df-so 5532  df-fr 5576  df-we 5578

This theorem is referenced by:  wefrc  5617  trssord  6328  ordelord  6333  dford5  7724  omsinds  7827  fnwelem  8071  dfrecs3  8302  ordtypelem8  9436  oismo  9451  cantnfcl  9582  infxpenlem  9926  ac10ct  9947  dfac12lem2  10058  cflim2  10176  cofsmo  10182  hsmexlem1  10339  smobeth  10499  canthwelem  10563  gruina  10731  ltwefz  13888  welb  37715  dnwech  43021  aomclem4  43030  dfac11  43035  oaun3lem1  43347  onfrALTlem3  44518  onfrALTlem3VD  44860