![]() |
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 5635 | . 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | |
2 | 1 | simplbi 496 | 1 ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 Or wor 5589 Fr wfr 5630 We wwe 5632 |
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 206 df-an 395 df-we 5635 |
This theorem is referenced by: wefrc 5672 wereu 5674 wereu2 5675 tz6.26 6355 wfi 6358 wfisg 6361 wfis2fg 6364 ordfr 6386 wexp 8135 wfrlem14OLD 8343 wfrfun 8353 wfrresex 8354 wfr2a 8355 wfr1 8356 wofib 9570 wemapso 9576 wemapso2lem 9577 cflim2 10288 fpwwe2lem11 10666 fpwwe2lem12 10667 fpwwe2 10668 welb 37340 fnwe2lem2 42617 onfrALTlem3 44125 onfrALTlem3VD 44468 |
Copyright terms: Public domain | W3C validator |