Definition df-fr 5640

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

This definition is referenced by:  dffr6  5643  friOLD  5646  dffr2  5649  dffr2ALT  5650  frss  5652  freq1  5655  nffr  5661  frinxp  5770  frsn  5775  f1oweALT  7995  frxp  8149  frxp2  8167  frxp3  8174  frfi  9318  fpwwe2lem11  10678  fpwwe2lem12  10679  lrrecfr  27990  bnj1154  34991  dffr5  35733  dfon2lem9  35772  weiunfr  36449  finorwe  37364  fin2so  37593  fnwe2  43041