MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fr Structured version   Visualization version   GIF version

Definition df-fr 5508
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5514 and dffr3 5956. A class is called well-founded when the membership relation E (see df-eprel 5459) is well-founded on it, that is, 𝐴 is well-founded if E Fr 𝐴 (some sources request that the membership relation be well-founded on its transitive closure). (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
df-fr (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
Distinct variable groups:   𝑥,𝑦,𝑧,𝑅   𝑥,𝐴,𝑦,𝑧

Detailed syntax breakdown of Definition df-fr
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wfr 5505 . 2 wff 𝑅 Fr 𝐴
4 vx . . . . . . 7 setvar 𝑥
54cv 1527 . . . . . 6 class 𝑥
65, 1wss 3935 . . . . 5 wff 𝑥𝐴
7 c0 4290 . . . . . 6 class
85, 7wne 3016 . . . . 5 wff 𝑥 ≠ ∅
96, 8wa 396 . . . 4 wff (𝑥𝐴𝑥 ≠ ∅)
10 vz . . . . . . . . 9 setvar 𝑧
1110cv 1527 . . . . . . . 8 class 𝑧
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1527 . . . . . . . 8 class 𝑦
1411, 13, 2wbr 5058 . . . . . . 7 wff 𝑧𝑅𝑦
1514wn 3 . . . . . 6 wff ¬ 𝑧𝑅𝑦
1615, 10, 5wral 3138 . . . . 5 wff 𝑧𝑥 ¬ 𝑧𝑅𝑦
1716, 12, 5wrex 3139 . . . 4 wff 𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦
189, 17wi 4 . . 3 wff ((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
1918, 4wal 1526 . 2 wff 𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
203, 19wb 207 1 wff (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
Colors of variables: wff setvar class
This definition is referenced by:  fri  5511  dffr2  5514  frss  5516  freq1  5519  nffr  5523  frinxp  5628  frsn  5633  f1oweALT  7664  frxp  7811  frfi  8752  fpwwe2lem12  10052  fpwwe2lem13  10053  bnj1154  32169  dffr5  32887  dfon2lem9  32934  finorwe  34546  fin2so  34761  fnwe2  39533
  Copyright terms: Public domain W3C validator