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