Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-frind | Unicode version |
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 . (Contributed by Jim Kingdon and Mario Carneiro, 21-Sep-2021.) |
Ref | Expression |
---|---|
df-frind | FrFor |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 | |
2 | cR | . . 3 | |
3 | 1, 2 | wfr 4313 | . 2 |
4 | vs | . . . . 5 | |
5 | 4 | cv 1347 | . . . 4 |
6 | 1, 2, 5 | wfrfor 4312 | . . 3 FrFor |
7 | 6, 4 | wal 1346 | . 2 FrFor |
8 | 3, 7 | wb 104 | 1 FrFor |
Colors of variables: wff set class |
This definition is referenced by: freq1 4329 freq2 4331 nffr 4334 frirrg 4335 fr0 4336 frind 4337 zfregfr 4558 |
Copyright terms: Public domain | W3C validator |