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

Definition df-frfor 4260
Description: Define the well-founded relation predicate where 𝐴 might be a proper class. By passing in 𝑆 we allow it potentially to be a proper class rather than a set. (Contributed by Jim Kingdon and Mario Carneiro, 22-Sep-2021.)
Assertion
Ref Expression
df-frfor ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆) → 𝐴𝑆))
Distinct variable groups:   𝑥,𝑦,𝑅   𝑥,𝐴,𝑦   𝑥,𝑆,𝑦

Detailed syntax breakdown of Definition df-frfor
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
3 cS . . 3 class 𝑆
41, 2, 3wfrfor 4256 . 2 wff FrFor 𝑅𝐴𝑆
5 vy . . . . . . . . 9 setvar 𝑦
65cv 1331 . . . . . . . 8 class 𝑦
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1331 . . . . . . . 8 class 𝑥
96, 8, 2wbr 3936 . . . . . . 7 wff 𝑦𝑅𝑥
106, 3wcel 1481 . . . . . . 7 wff 𝑦𝑆
119, 10wi 4 . . . . . 6 wff (𝑦𝑅𝑥𝑦𝑆)
1211, 5, 1wral 2417 . . . . 5 wff 𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆)
138, 3wcel 1481 . . . . 5 wff 𝑥𝑆
1412, 13wi 4 . . . 4 wff (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆)
1514, 7, 1wral 2417 . . 3 wff 𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆)
161, 3wss 3075 . . 3 wff 𝐴𝑆
1715, 16wi 4 . 2 wff (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆) → 𝐴𝑆)
184, 17wb 104 1 wff ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆) → 𝐴𝑆))
Colors of variables: wff set class
This definition is referenced by:  frforeq1  4272  frforeq2  4274  frforeq3  4276  nffrfor  4277  frirrg  4279  fr0  4280  frind  4281  zfregfr  4495
  Copyright terms: Public domain W3C validator