Theorem wess 5638

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 5616	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Fr 𝐵 → 𝑅 Fr 𝐴))
2		soss 5580	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴))
3	1, 2	anim12d 620	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵) → (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)))
4		df-we 5607	. 2 ⊢ (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵))
5		df-we 5607	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
6	3, 4, 5	3imtr4g 299	1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 We 𝐵 → 𝑅 We 𝐴))

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3907   Or wor 5559   Fr wfr 5602   We wwe 5604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3080  df-ss 3924  df-po 5560  df-so 5561  df-fr 5605  df-we 5607

This theorem is referenced by:  wefrc  5646  trssord  6367  ordelord  6372  dford5  7771  omsinds  7871  fnwelem  8115  dfrecs3  8347  ordtypelem8  9475  oismo  9490  cantnfcl  9624  infxpenlem  9985  ac10ct  10006  dfac12lem2  10116  cflim2  10235  cofsmo  10241  hsmexlem1  10398  smobeth  10559  canthwelem  10623  gruina  10791  ltwefz  13990  wevonprcf1o  35468  welb  38247  dnwech  43637  aomclem4  43646  dfac11  43651  oaun3lem1  43963  onfrALTlem3  45118  onfrALTlem3VD  45460