Theorem wess 5625

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

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3913   Or wor 5549   Fr wfr 5590   We wwe 5592

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-v 3448  df-in 3920  df-ss 3930  df-po 5550  df-so 5551  df-fr 5593  df-we 5595

This theorem is referenced by:  wefrc  5632  trssord  6339  ordelord  6344  dford5  7723  omsinds  7828  omsindsOLD  7829  fnwelem  8068  wfrlem5OLD  8264  dfrecs3  8323  dfrecs3OLD  8324  ordtypelem8  9470  oismo  9485  cantnfcl  9612  infxpenlem  9958  ac10ct  9979  dfac12lem2  10089  cflim2  10208  cofsmo  10214  hsmexlem1  10371  smobeth  10531  canthwelem  10595  gruina  10763  ltwefz  13878  welb  36268  dnwech  41433  aomclem4  41442  dfac11  41447  oaun3lem1  41767  onfrALTlem3  42948  onfrALTlem3VD  43291