Definition df-fr 5567

Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5575 and dffr3 6045. A class is called well-founded when the membership relation E (see df-eprel 5514) 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 5564	. 2 wff 𝑅 Fr 𝐴
4		vx	. . . . . . 7 setvar 𝑥
5	4	cv 1540	. . . . . 6 class 𝑥
6	5, 1	wss 3900	. . . . 5 wff 𝑥 ⊆ 𝐴
7		c0 4281	. . . . . 6 class ∅
8	5, 7	wne 2926	. . . . 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 5089	. . . . . . 7 wff 𝑧𝑅𝑦
15	14	wn 3	. . . . . 6 wff ¬ 𝑧𝑅𝑦
16	15, 10, 5	wral 3045	. . . . 5 wff ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦
17	16, 12, 5	wrex 3054	. . . 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  5570  dffr2  5575  dffr2ALT  5576  frss  5578  freq1  5581  nffr  5587  frinxp  5697  frsn  5702  f1oweALT  7899  frxp  8051  frxp2  8069  frxp3  8076  frfi  9164  fpwwe2lem11  10524  fpwwe2lem12  10525  lrrecfr  27879  bnj1154  35001  vonf1owev  35120  dffr5  35766  dfon2lem9  35804  weiunfr  36480  finorwe  37395  fin2so  37626  fnwe2  43065