Theorem wess 5647

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

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3904   Or wor 5568   Fr wfr 5611   We wwe 5613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938

This theorem depends on definitions:  df-bi 210  df-an 401  df-ral 3078  df-ss 3921  df-po 5569  df-so 5570  df-fr 5614  df-we 5616

This theorem is referenced by:  wefrc  5655  trssord  6377  ordelord  6382  dford5  7782  omsinds  7882  fnwelem  8126  dfrecs3  8358  ordtypelem8  9486  oismo  9501  cantnfcl  9635  infxpenlem  9996  ac10ct  10017  dfac12lem2  10127  cflim2  10246  cofsmo  10252  hsmexlem1  10409  smobeth  10570  canthwelem  10634  gruina  10802  ltwefz  13999  wevonprcf1o  35563  welb  38353  dnwech  43745  aomclem4  43754  dfac11  43759  oaun3lem1  44071  onfrALTlem3  45223  onfrALTlem3VD  45565