Theorem wess 5645

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3902   Or wor 5566   Fr wfr 5609   We wwe 5611

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3079  df-ss 3919  df-po 5567  df-so 5568  df-fr 5612  df-we 5614

This theorem is used by:  wefrc  5653  trssord  6378  ordelord  6383  f1we  7359  dford5  7786  omsinds  7886  fnwelem  8132  dfrecs3  8364  ordtypelem8  9500  oismo  9515  cantnfcl  9649  infxpenlem  10019  ac10ct  10040  dfac12lem2  10150  cflim2  10268  cofsmo  10274  hsmexlem1  10431  smobeth  10598  canthwelem  10662  gruina  10830  ltwefz  14029  wevonprcf1o  35712  welb  38488  aomclem4  43900  dfac11  43905  oaun3lem1  44217  onfrALTlem3  45369  onfrALTlem3VD  45711