Theorem wess 5611

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

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3890   Or wor 5532   Fr wfr 5575   We wwe 5577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ral 3055  df-ss 3907  df-po 5533  df-so 5534  df-fr 5578  df-we 5580

This theorem is referenced by:  wefrc  5619  trssord  6334  ordelord  6339  dford5  7734  omsinds  7834  fnwelem  8078  dfrecs3  8309  ordtypelem8  9437  oismo  9452  cantnfcl  9586  infxpenlem  9933  ac10ct  9954  dfac12lem2  10065  cflim2  10183  cofsmo  10189  hsmexlem1  10346  smobeth  10507  canthwelem  10571  gruina  10739  ltwefz  13923  welb  38104  dnwech  43494  aomclem4  43503  dfac11  43508  oaun3lem1  43820  onfrALTlem3  44989  onfrALTlem3VD  45331