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

Metamath Proof Explorer

Definition df-fr

Description: Define the well-founded relation predicate. Definition 6.24(1) of TakeutiZaring p. 30. For alternate definitions, see dffr2 and dffr3 . A class is called well-founded when the membership relation _E (see df-eprel ) is well-founded on it, that is, A is well-founded if _E Fr A (some sources request that the membership relation be well-founded on its transitive closure). (Contributed by NM, 3-Apr-1994)

Ref Expression
Assertion df-fr ⊢ R Fr A ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR class R
1 cA class A
2 1 0 wfr wff R Fr A
3 vx setvar x
4 3 cv setvar x
5 4 1 wss wff x ⊆ A
6 c0 class ∅
7 4 6 wne wff x ≠ ∅
8 5 7 wa wff x ⊆ A ∧ x ≠ ∅
9 vy setvar y
10 vz setvar z
11 10 cv setvar z
12 9 cv setvar y
13 11 12 0 wbr wff z R y
14 13 wn wff ¬ z R y
15 14 10 4 wral wff ∀ z ∈ x ¬ z R y
16 15 9 4 wrex wff ∃ y ∈ x ∀ z ∈ x ¬ z R y
17 8 16 wi wff x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
18 17 3 wal wff ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y
19 2 18 wb wff R Fr A ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z R y