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

Definition df-frfor 4068
 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 4064 . 2 wff FrFor 𝑅𝐴𝑆
5 vy . . . . . . . . 9 setvar 𝑦
65cv 1242 . . . . . . . 8 class 𝑦
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1242 . . . . . . . 8 class 𝑥
96, 8, 2wbr 3764 . . . . . . 7 wff 𝑦𝑅𝑥
106, 3wcel 1393 . . . . . . 7 wff 𝑦𝑆
119, 10wi 4 . . . . . 6 wff (𝑦𝑅𝑥𝑦𝑆)
1211, 5, 1wral 2306 . . . . 5 wff 𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆)
138, 3wcel 1393 . . . . 5 wff 𝑥𝑆
1412, 13wi 4 . . . 4 wff (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆)
1514, 7, 1wral 2306 . . 3 wff 𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆)
161, 3wss 2917 . . 3 wff 𝐴𝑆
1715, 16wi 4 . 2 wff (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆) → 𝐴𝑆)
184, 17wb 98 1 wff ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆) → 𝐴𝑆))
 Colors of variables: wff set class This definition is referenced by:  frforeq1  4080  frforeq2  4082  frforeq3  4084  nffrfor  4085  frirrg  4087  fr0  4088  frind  4089  zfregfr  4298
 Copyright terms: Public domain W3C validator