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 ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR ⊢ 𝑅
1 cA ⊢ 𝐴
2 1 0 wfr ⊢ 𝑅 Fr 𝐴
3 vx ⊢ 𝑥
4 3 cv ⊢ 𝑥
5 4 1 wss ⊢ 𝑥 ⊆ 𝐴
6 c0 ⊢ ∅
7 4 6 wne ⊢ 𝑥 ≠ ∅
8 5 7 wa ⊢ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ )
9 vy ⊢ 𝑦
10 vz ⊢ 𝑧
11 10 cv ⊢ 𝑧
12 9 cv ⊢ 𝑦
13 11 12 0 wbr ⊢ 𝑧 𝑅 𝑦
14 13 wn ⊢ ¬ 𝑧 𝑅 𝑦
15 14 10 4 wral ⊢ ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦
16 15 9 4 wrex ⊢ ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦
17 8 16 wi ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
18 17 3 wal ⊢ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 )
19 2 18 wb ⊢ ( 𝑅 Fr 𝐴 ↔ ∀ 𝑥 ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑥 ∀ 𝑧 ∈ 𝑥 ¬ 𝑧 𝑅 𝑦 ) )