![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-frind | GIF 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 Fr. (Contributed by Jim Kingdon and Mario Carneiro, 21-Sep-2021.) |
Ref | Expression |
---|---|
df-frind | ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cR | . . 3 class 𝑅 | |
3 | 1, 2 | wfr 4179 | . 2 wff 𝑅 Fr 𝐴 |
4 | vs | . . . . 5 setvar 𝑠 | |
5 | 4 | cv 1295 | . . . 4 class 𝑠 |
6 | 1, 2, 5 | wfrfor 4178 | . . 3 wff FrFor 𝑅𝐴𝑠 |
7 | 6, 4 | wal 1294 | . 2 wff ∀𝑠 FrFor 𝑅𝐴𝑠 |
8 | 3, 7 | wb 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 |