Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > wefr | Structured version Visualization version GIF version |
Description: A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.) |
Ref | Expression |
---|---|
wefr | ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-we 4999 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
2 | 1 | simplbi 475 | 1 ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 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 |
This theorem depends on definitions: df-bi 196 df-an 385 df-we 4999 |
This theorem is referenced by: wefrc 5032 wereu 5034 wereu2 5035 ordfr 5655 wexp 7178 wfrlem14 7315 wofib 8333 wemapso 8339 wemapso2lem 8340 cflim2 8968 fpwwe2lem12 9342 fpwwe2lem13 9343 fpwwe2 9344 welb 32701 fnwe2lem2 36639 onfrALTlem3 37780 onfrALTlem3VD 38145 |
Copyright terms: Public domain | W3C validator |