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

Definition df-frfor 4291
Description: Define the well-founded relation predicate where  A might be a proper class. By passing in  S 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  R A S  <->  ( A. x  e.  A  ( A. y  e.  A  (
y R x  -> 
y  e.  S )  ->  x  e.  S
)  ->  A  C_  S
) )
Distinct variable groups:    x, y, R   
x, A, y    x, S, y

Detailed syntax breakdown of Definition df-frfor
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
3 cS . . 3  class  S
41, 2, 3wfrfor 4287 . 2  wff FrFor  R A S
5 vy . . . . . . . . 9  setvar  y
65cv 1334 . . . . . . . 8  class  y
7 vx . . . . . . . . 9  setvar  x
87cv 1334 . . . . . . . 8  class  x
96, 8, 2wbr 3965 . . . . . . 7  wff  y R x
106, 3wcel 2128 . . . . . . 7  wff  y  e.  S
119, 10wi 4 . . . . . 6  wff  ( y R x  ->  y  e.  S )
1211, 5, 1wral 2435 . . . . 5  wff  A. y  e.  A  ( y R x  ->  y  e.  S )
138, 3wcel 2128 . . . . 5  wff  x  e.  S
1412, 13wi 4 . . . 4  wff  ( A. y  e.  A  (
y R x  -> 
y  e.  S )  ->  x  e.  S
)
1514, 7, 1wral 2435 . . 3  wff  A. x  e.  A  ( A. y  e.  A  (
y R x  -> 
y  e.  S )  ->  x  e.  S
)
161, 3wss 3102 . . 3  wff  A  C_  S
1715, 16wi 4 . 2  wff  ( A. x  e.  A  ( A. y  e.  A  ( y R x  ->  y  e.  S
)  ->  x  e.  S )  ->  A  C_  S )
184, 17wb 104 1  wff  (FrFor  R A S  <->  ( A. x  e.  A  ( A. y  e.  A  (
y R x  -> 
y  e.  S )  ->  x  e.  S
)  ->  A  C_  S
) )
Colors of variables: wff set class
This definition is referenced by:  frforeq1  4303  frforeq2  4305  frforeq3  4307  nffrfor  4308  frirrg  4310  fr0  4311  frind  4312  zfregfr  4533
  Copyright terms: Public domain W3C validator