Theorem wess 5671

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3951   Or wor 5591   Fr wfr 5634   We wwe 5636

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 3062  df-ss 3968  df-po 5592  df-so 5593  df-fr 5637  df-we 5639

This theorem is referenced by:  wefrc  5679  trssord  6401  ordelord  6406  dford5  7804  omsinds  7908  fnwelem  8156  wfrlem5OLD  8353  dfrecs3  8412  dfrecs3OLD  8413  ordtypelem8  9565  oismo  9580  cantnfcl  9707  infxpenlem  10053  ac10ct  10074  dfac12lem2  10185  cflim2  10303  cofsmo  10309  hsmexlem1  10466  smobeth  10626  canthwelem  10690  gruina  10858  ltwefz  14004  welb  37743  dnwech  43060  aomclem4  43069  dfac11  43074  oaun3lem1  43387  onfrALTlem3  44564  onfrALTlem3VD  44907