![]() |
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 5486 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Fr 𝐵 → 𝑅 Fr 𝐴)) | |
2 | soss 5457 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴)) | |
3 | 1, 2 | anim12d 611 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵) → (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))) |
4 | df-we 5480 | . 2 ⊢ (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵)) | |
5 | df-we 5480 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
6 | 3, 4, 5 | 3imtr4g 299 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 We 𝐵 → 𝑅 We 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 ⊆ wss 3881 Or wor 5437 Fr wfr 5475 We wwe 5477 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-ext 2770 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1782 df-sb 2070 df-clab 2777 df-cleq 2791 df-clel 2870 df-ral 3111 df-v 3443 df-in 3888 df-ss 3898 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 |
This theorem is referenced by: wefrc 5513 trssord 6176 ordelord 6181 omsinds 7580 fnwelem 7808 wfrlem5 7942 dfrecs3 7992 ordtypelem8 8973 oismo 8988 cantnfcl 9114 infxpenlem 9424 ac10ct 9445 dfac12lem2 9555 cflim2 9674 cofsmo 9680 hsmexlem1 9837 smobeth 9997 canthwelem 10061 gruina 10229 ltwefz 13326 dford5 33070 welb 35174 dnwech 39992 aomclem4 40001 dfac11 40006 onfrALTlem3 41250 onfrALTlem3VD 41593 |
Copyright terms: Public domain | W3C validator |