Theorem wess 5611

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3902   Or wor 5532   Fr wfr 5575   We wwe 5577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3053  df-ss 3919  df-po 5533  df-so 5534  df-fr 5578  df-we 5580

This theorem is referenced by:  wefrc  5619  trssord  6335  ordelord  6340  dford5  7731  omsinds  7831  fnwelem  8075  dfrecs3  8306  ordtypelem8  9434  oismo  9449  cantnfcl  9580  infxpenlem  9927  ac10ct  9948  dfac12lem2  10059  cflim2  10177  cofsmo  10183  hsmexlem1  10340  smobeth  10501  canthwelem  10565  gruina  10733  ltwefz  13890  welb  37908  dnwech  43326  aomclem4  43335  dfac11  43340  oaun3lem1  43652  onfrALTlem3  44821  onfrALTlem3VD  45163