Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Founded and well-ordering relations
wefr
Next ⟩
weso
Metamath Proof Explorer
Ascii
Structured
Theorem
wefr
Description:
A well-ordering is well-founded.
(Contributed by
NM
, 22-Apr-1994)
Ref
Expression
Assertion
wefr
⊢
(
𝑅
We
𝐴
→
𝑅
Fr
𝐴
)
Proof
Step
Hyp
Ref
Expression
1
df-we
⊢
(
𝑅
We
𝐴
↔ (
𝑅
Fr
𝐴
∧
𝑅
Or
𝐴
) )
2
1
simplbi
⊢
(
𝑅
We
𝐴
→
𝑅
Fr
𝐴
)