Definition df-fr 5612

Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5620 and dffr3 6099. A class is called well-founded when the membership relation E (see df-eprel 5559) 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 5609	. 2 wff 𝑅 Fr 𝐴
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1569	. . . . . 6 class 𝑥
6	5, 1	wss 3902	. . . . 5 wff 𝑥 ⊆ 𝐴
7		c0 4282	. . . . . 6 class ∅
8	5, 7	wne 2957	. . . . 5 wff 𝑥 ≠ ∅
9	6, 8	wa 401	. . . 4 wff (𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅)
10		vz	. . . . . . . . 9 setvar 𝑧
11	10	cv 1569	. . . . . . . 8 class 𝑧
12		vy	. . . . . . . . 9 setvar 𝑦
13	12	cv 1569	. . . . . . . 8 class 𝑦
14	11, 13, 2	wbr 5107	. . . . . . 7 wff 𝑧𝑅𝑦
15	14	wn 3	. . . . . 6 wff ¬ 𝑧𝑅𝑦
16	15, 10, 5	wral 3078	. . . . 5 wff ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦
17	16, 12, 5	wrex 3088	. . . 4 wff ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦
18	9, 17	wi 4	. . 3 wff ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)
19	18, 4	wal 1568	. 2 wff ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)
20	3, 19	wb 209	1 wff (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦))

This definition is used by:  dffr6  5615  dffr2  5620  dffr2ALT  5621  frss  5623  freq1  5626  nffr  5632  frinxp  5742  frsn  5747  f1oweALT  7973  frxp  8128  frxp2  8146  frxp3  8153  frfi  9259  fpwwe2lem11  10654  fpwwe2lem12  10655  lrrecfr  28216  bnj1154  35516  vonf1wev  35713  vonf1owevOLD  35715  dfon2lem9  36376  weiunfr  37094  finorwe  38144  fin2so  38369  fnwe2  43902