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

Definition df-frfor 4094
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 4090 . 2 wff FrFor 𝑅𝐴𝑆
5 vy . . . . . . . . 9 setvar 𝑦
65cv 1284 . . . . . . . 8 class 𝑦
7 vx . . . . . . . . 9 setvar 𝑥
87cv 1284 . . . . . . . 8 class 𝑥
96, 8, 2wbr 3793 . . . . . . 7 wff 𝑦𝑅𝑥
106, 3wcel 1434 . . . . . . 7 wff 𝑦𝑆
119, 10wi 4 . . . . . 6 wff (𝑦𝑅𝑥𝑦𝑆)
1211, 5, 1wral 2349 . . . . 5 wff 𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆)
138, 3wcel 1434 . . . . 5 wff 𝑥𝑆
1412, 13wi 4 . . . 4 wff (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆)
1514, 7, 1wral 2349 . . 3 wff 𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆)
161, 3wss 2974 . . 3 wff 𝐴𝑆
1715, 16wi 4 . 2 wff (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆) → 𝐴𝑆)
184, 17wb 103 1 wff ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆) → 𝐴𝑆))
Colors of variables: wff set class
This definition is referenced by:  frforeq1  4106  frforeq2  4108  frforeq3  4110  nffrfor  4111  frirrg  4113  fr0  4114  frind  4115  zfregfr  4324
  Copyright terms: Public domain W3C validator