Theorem wess 5636

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3895   Or wor 5557   Fr wfr 5600   We wwe 5602

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ral 3077  df-ss 3896  df-po 5558  df-so 5559  df-fr 5603  df-we 5605

This theorem is used by:  wefrc  5644  trssord  6379  ordelord  6384  f1we  7363  dford5  7798  omsinds  7898  fnwelem  8143  dfrecs3  8381  ordtypelem8  9520  oismo  9535  cantnfcl  9669  infxpenlem  10093  ac10ct  10114  dfac12lem2  10224  cflim2  10342  cofsmo  10348  hsmexlem1  10505  smobeth  10672  canthwelem  10736  gruina  10904  ltwefz  14107  onf1we  35764  wevsev  35953  wevonprcf1o  35954  vonf1onprcf1ac  35956  onprcf1acwevdlem1  35957  onprcf1acwevdlem2  35958  onprcr  36531  welb  38746  aomclem4  44135  dfac11  44140  oaun3lem1  44452  onfrALTlem3  45603  onfrALTlem3VD  45945