Theorem wess 5648

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

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3911   Or wor 5569   Fr wfr 5612   We wwe 5614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3086  df-ss 3928  df-po 5570  df-so 5571  df-fr 5615  df-we 5617

This theorem is referenced by:  wefrc  5656  trssord  6378  ordelord  6383  dford5  7783  omsinds  7883  fnwelem  8127  dfrecs3  8359  ordtypelem8  9487  oismo  9502  cantnfcl  9636  infxpenlem  9997  ac10ct  10018  dfac12lem2  10128  cflim2  10247  cofsmo  10253  hsmexlem1  10410  smobeth  10571  canthwelem  10635  gruina  10803  ltwefz  13999  wevonprcf1o  35530  welb  38310  dnwech  43702  aomclem4  43711  dfac11  43716  oaun3lem1  44028  onfrALTlem3  45180  onfrALTlem3VD  45522