Theorem wess 5633

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3898   Or wor 5554   Fr wfr 5597   We wwe 5599

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 3077  df-ss 3915  df-po 5555  df-so 5556  df-fr 5600  df-we 5602

This theorem is used by:  wefrc  5641  trssord  6368  ordelord  6373  f1we  7351  dford5  7781  omsinds  7881  fnwelem  8126  dfrecs3  8358  ordtypelem8  9497  oismo  9512  cantnfcl  9646  infxpenlem  10064  ac10ct  10085  dfac12lem2  10195  cflim2  10313  cofsmo  10319  hsmexlem1  10476  smobeth  10643  canthwelem  10707  gruina  10875  ltwefz  14075  wevonprcf1o  35817  welb  38590  aomclem4  44002  dfac11  44007  oaun3lem1  44319  onfrALTlem3  45471  onfrALTlem3VD  45813