![]() |
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 5365 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
2 | 1 | simplbi 490 | 1 ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Or wor 5322 Fr wfr 5360 We wwe 5362 |
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 199 df-an 388 df-we 5365 |
This theorem is referenced by: wefrc 5398 wereu 5400 wereu2 5401 ordfr 6042 wexp 7628 wfrlem14 7771 wofib 8803 wemapso 8809 wemapso2lem 8810 cflim2 9482 fpwwe2lem12 9860 fpwwe2lem13 9861 fpwwe2 9862 welb 34486 fnwe2lem2 39081 onfrALTlem3 40331 onfrALTlem3VD 40674 |
Copyright terms: Public domain | W3C validator |