Definition df-frind 4427

Description: Define the well-founded relation predicate. In the presence of excluded middle, there are a variety of equivalent ways to define this. In our case, this definition, in terms of an inductive principle, works better than one along the lines of "there is an element which is minimal when A is ordered by R". Because 𝑠 is constrained to be a set (not a proper class) here, sometimes it may be necessary to use FrFor directly rather than via Fr. (Contributed by Jim Kingdon and Mario Carneiro, 21-Sep-2021.)

Assertion

Ref	Expression
df-frind	⊢ (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠)

Distinct variable groups:   𝑅,𝑠   𝐴,𝑠

Detailed syntax breakdown of Definition df-frind

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wfr 4423	. 2 wff 𝑅 Fr 𝐴
4		vs	. . . . 5 setvar 𝑠
5	4	cv 1394	. . . 4 class 𝑠
6	1, 2, 5	wfrfor 4422	. . 3 wff FrFor 𝑅𝐴𝑠
7	6, 4	wal 1393	. 2 wff ∀𝑠 FrFor 𝑅𝐴𝑠
8	3, 7	wb 105	1 wff (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠)

This definition is referenced by:  freq1  4439  freq2  4441  nffr  4444  frirrg  4445  fr0  4446  frind  4447  zfregfr  4670