Definition df-fr 5606

Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5615 and dffr3 6086. A class is called well-founded when the membership relation E (see df-eprel 5553) 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 5603	. 2 wff 𝑅 Fr 𝐴
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1539	. . . . . 6 class 𝑥
6	5, 1	wss 3926	. . . . 5 wff 𝑥 ⊆ 𝐴
7		c0 4308	. . . . . 6 class ∅
8	5, 7	wne 2932	. . . . 5 wff 𝑥 ≠ ∅
9	6, 8	wa 395	. . . 4 wff (𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅)
10		vz	. . . . . . . . 9 setvar 𝑧
11	10	cv 1539	. . . . . . . 8 class 𝑧
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1539	. . . . . . . 8 class 𝑦
14	11, 13, 2	wbr 5119	. . . . . . 7 wff 𝑧𝑅𝑦
15	14	wn 3	. . . . . 6 wff ¬ 𝑧𝑅𝑦
16	15, 10, 5	wral 3051	. . . . 5 wff ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦
17	16, 12, 5	wrex 3060	. . . 4 wff ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦
18	9, 17	wi 4	. . 3 wff ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)
19	18, 4	wal 1538	. 2 wff ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)
20	3, 19	wb 206	1 wff (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))

This definition is referenced by:  dffr6  5609  friOLD  5612  dffr2  5615  dffr2ALT  5616  frss  5618  freq1  5621  nffr  5627  frinxp  5737  frsn  5742  f1oweALT  7969  frxp  8123  frxp2  8141  frxp3  8148  frfi  9291  fpwwe2lem11  10653  fpwwe2lem12  10654  lrrecfr  27893  bnj1154  34976  dffr5  35717  dfon2lem9  35755  weiunfr  36431  finorwe  37346  fin2so  37577  fnwe2  43024