Theorem wess 5640

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3926   Or wor 5560   Fr wfr 5603   We wwe 5605

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 3052  df-ss 3943  df-po 5561  df-so 5562  df-fr 5606  df-we 5608

This theorem is referenced by:  wefrc  5648  trssord  6369  ordelord  6374  dford5  7778  omsinds  7882  fnwelem  8130  wfrlem5OLD  8327  dfrecs3  8386  dfrecs3OLD  8387  ordtypelem8  9539  oismo  9554  cantnfcl  9681  infxpenlem  10027  ac10ct  10048  dfac12lem2  10159  cflim2  10277  cofsmo  10283  hsmexlem1  10440  smobeth  10600  canthwelem  10664  gruina  10832  ltwefz  13981  welb  37760  dnwech  43072  aomclem4  43081  dfac11  43086  oaun3lem1  43398  onfrALTlem3  44569  onfrALTlem3VD  44911