This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-we

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 . (Contributed by NM, 3-Apr-1994)

Ref Expression
Assertion df-we ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR ⊢ 𝑅
1 cA ⊢ 𝐴
2 1 0 wwe ⊢ 𝑅 We 𝐴
3 1 0 wfr ⊢ 𝑅 Fr 𝐴
4 1 0 wor ⊢ 𝑅 Or 𝐴
5 3 4 wa ⊢ ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 )
6 2 5 wb ⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 ) )