Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > wess | Structured version Visualization version GIF version |
Description: Subset theorem for the well-ordering predicate. Exercise 4 of [TakeutiZaring] p. 31. (Contributed by NM, 19-Apr-1994.) |
Ref | Expression |
---|---|
wess | ⊢ (𝐴 ⊆ 𝐵 → (𝑅 We 𝐵 → 𝑅 We 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frss 5005 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Fr 𝐵 → 𝑅 Fr 𝐴)) | |
2 | soss 4977 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴)) | |
3 | 1, 2 | anim12d 584 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵) → (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))) |
4 | df-we 4999 | . 2 ⊢ (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵)) | |
5 | df-we 4999 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
6 | 3, 4, 5 | 3imtr4g 284 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 We 𝐵 → 𝑅 We 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ⊆ wss 3540 Or wor 4958 Fr wfr 4994 We wwe 4996 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-ral 2901 df-in 3547 df-ss 3554 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 |
This theorem is referenced by: wefrc 5032 trssord 5657 ordelord 5662 omsinds 6976 fnwelem 7179 wfrlem5 7306 dfrecs3 7356 ordtypelem8 8313 oismo 8328 cantnfcl 8447 infxpenlem 8719 ac10ct 8740 dfac12lem2 8849 cflim2 8968 cofsmo 8974 hsmexlem1 9131 smobeth 9287 canthwelem 9351 gruina 9519 ltwefz 12624 welb 32701 dnwech 36636 aomclem4 36645 dfac11 36650 onfrALTlem3 37780 onfrALTlem3VD 38145 |
Copyright terms: Public domain | W3C validator |