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 5556 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Fr 𝐵 → 𝑅 Fr 𝐴)) | |
2 | soss 5523 | . . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴)) | |
3 | 1, 2 | anim12d 609 | . 2 ⊢ (𝐴 ⊆ 𝐵 → ((𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵) → (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))) |
4 | df-we 5546 | . 2 ⊢ (𝑅 We 𝐵 ↔ (𝑅 Fr 𝐵 ∧ 𝑅 Or 𝐵)) | |
5 | df-we 5546 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
6 | 3, 4, 5 | 3imtr4g 296 | 1 ⊢ (𝐴 ⊆ 𝐵 → (𝑅 We 𝐵 → 𝑅 We 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ⊆ wss 3887 Or wor 5502 Fr wfr 5541 We wwe 5543 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3069 df-v 3434 df-in 3894 df-ss 3904 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 |
This theorem is referenced by: wefrc 5583 trssord 6283 ordelord 6288 omsinds 7733 omsindsOLD 7734 fnwelem 7972 wfrlem5OLD 8144 dfrecs3 8203 dfrecs3OLD 8204 ordtypelem8 9284 oismo 9299 cantnfcl 9425 infxpenlem 9769 ac10ct 9790 dfac12lem2 9900 cflim2 10019 cofsmo 10025 hsmexlem1 10182 smobeth 10342 canthwelem 10406 gruina 10574 ltwefz 13683 dford5 33671 welb 35894 dnwech 40873 aomclem4 40882 dfac11 40887 onfrALTlem3 42164 onfrALTlem3VD 42507 |
Copyright terms: Public domain | W3C validator |