Theorem wess 5646

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ⊆ wss 3904   Or wor 5567   Fr wfr 5610   We wwe 5612

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939

This proof depends on definitions:  df-bi 210  df-an 401  df-ral 3079  df-ss 3921  df-po 5568  df-so 5569  df-fr 5613  df-we 5615

This theorem is used by:  wefrc  5654  trssord  6377  ordelord  6382  f1we  7353  dford5  7781  omsinds  7881  fnwelem  8125  dfrecs3  8357  ordtypelem8  9485  oismo  9500  cantnfcl  9634  infxpenlem  10004  ac10ct  10025  dfac12lem2  10135  cflim2  10253  cofsmo  10259  hsmexlem1  10416  smobeth  10577  canthwelem  10641  gruina  10809  ltwefz  14006  wevonprcf1o  35605  welb  38415  aomclem4  43812  dfac11  43817  oaun3lem1  44129  onfrALTlem3  45281  onfrALTlem3VD  45623