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

Definition df-frind 4224
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  s 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  |-  ( R  Fr  A  <->  A. sFrFor  R A s )
Distinct variable groups:    R, s    A, s

Detailed syntax breakdown of Definition df-frind
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2wfr 4220 . 2  wff  R  Fr  A
4 vs . . . . 5  setvar  s
54cv 1315 . . . 4  class  s
61, 2, 5wfrfor 4219 . . 3  wff FrFor  R A s
76, 4wal 1314 . 2  wff  A. sFrFor  R A s
83, 7wb 104 1  wff  ( R  Fr  A  <->  A. sFrFor  R A s )
Colors of variables: wff set class
This definition is referenced by:  freq1  4236  freq2  4238  nffr  4241  frirrg  4242  fr0  4243  frind  4244  zfregfr  4458
  Copyright terms: Public domain W3C validator