Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-frind GIF version

Definition df-frind 4183
 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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wfr 4179 . 2 wff 𝑅 Fr 𝐴
4 vs . . . . 5 setvar 𝑠
54cv 1295 . . . 4 class 𝑠
61, 2, 5wfrfor 4178 . . 3 wff FrFor 𝑅𝐴𝑠
76, 4wal 1294 . 2 wff 𝑠 FrFor 𝑅𝐴𝑠
83, 7wb 104 1 wff (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠)
 Colors of variables: wff set class This definition is referenced by:  freq1  4195  freq2  4197  nffr  4200  frirrg  4201  fr0  4202  frind  4203  zfregfr  4417
 Copyright terms: Public domain W3C validator