Definition df-fr 5572

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

Assertion

Ref	Expression
df-fr	⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))

Distinct variable groups:   𝑥,𝑦,𝑧,𝑅   𝑥,𝐴,𝑦,𝑧

Detailed syntax breakdown of Definition df-fr

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wfr 5569	. 2 wff 𝑅 Fr 𝐴
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1540	. . . . . 6 class 𝑥
6	5, 1	wss 3897	. . . . 5 wff 𝑥 ⊆ 𝐴
7		c0 4282	. . . . . 6 class ∅
8	5, 7	wne 2928	. . . . 5 wff 𝑥 ≠ ∅
9	6, 8	wa 395	. . . 4 wff (𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅)
10		vz	. . . . . . . . 9 setvar 𝑧
11	10	cv 1540	. . . . . . . 8 class 𝑧
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1540	. . . . . . . 8 class 𝑦
14	11, 13, 2	wbr 5093	. . . . . . 7 wff 𝑧𝑅𝑦
15	14	wn 3	. . . . . 6 wff ¬ 𝑧𝑅𝑦
16	15, 10, 5	wral 3047	. . . . 5 wff ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦
17	16, 12, 5	wrex 3056	. . . 4 wff ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦
18	9, 17	wi 4	. . 3 wff ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)
19	18, 4	wal 1539	. 2 wff ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)
20	3, 19	wb 206	1 wff (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))

This definition is referenced by:  dffr6  5575  dffr2  5580  dffr2ALT  5581  frss  5583  freq1  5586  nffr  5592  frinxp  5702  frsn  5707  f1oweALT  7910  frxp  8062  frxp2  8080  frxp3  8087  frfi  9175  fpwwe2lem11  10538  fpwwe2lem12  10539  lrrecfr  27892  bnj1154  35018  vonf1owev  35159  dffr5  35805  dfon2lem9  35840  weiunfr  36518  finorwe  37433  fin2so  37653  fnwe2  43151