Theorem wess 5627

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3917   Or wor 5548   Fr wfr 5591   We wwe 5593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ral 3046  df-ss 3934  df-po 5549  df-so 5550  df-fr 5594  df-we 5596

This theorem is referenced by:  wefrc  5635  trssord  6352  ordelord  6357  dford5  7763  omsinds  7866  fnwelem  8113  dfrecs3  8344  ordtypelem8  9485  oismo  9500  cantnfcl  9627  infxpenlem  9973  ac10ct  9994  dfac12lem2  10105  cflim2  10223  cofsmo  10229  hsmexlem1  10386  smobeth  10546  canthwelem  10610  gruina  10778  ltwefz  13935  welb  37737  dnwech  43044  aomclem4  43053  dfac11  43058  oaun3lem1  43370  onfrALTlem3  44541  onfrALTlem3VD  44883