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 5270
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5276 and dffr3 5708. (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 5267 . 2 wff 𝑅 Fr 𝐴
4 vx . . . . . . 7 setvar 𝑥
54cv 1636 . . . . . 6 class 𝑥
65, 1wss 3769 . . . . 5 wff 𝑥𝐴
7 c0 4116 . . . . . 6 class
85, 7wne 2978 . . . . 5 wff 𝑥 ≠ ∅
96, 8wa 384 . . . 4 wff (𝑥𝐴𝑥 ≠ ∅)
10 vz . . . . . . . . 9 setvar 𝑧
1110cv 1636 . . . . . . . 8 class 𝑧
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1636 . . . . . . . 8 class 𝑦
1411, 13, 2wbr 4844 . . . . . . 7 wff 𝑧𝑅𝑦
1514wn 3 . . . . . 6 wff ¬ 𝑧𝑅𝑦
1615, 10, 5wral 3096 . . . . 5 wff 𝑧𝑥 ¬ 𝑧𝑅𝑦
1716, 12, 5wrex 3097 . . . 4 wff 𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦
189, 17wi 4 . . 3 wff ((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
1918, 4wal 1635 . 2 wff 𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
203, 19wb 197 1 wff (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
Colors of variables: wff setvar class
This definition is referenced by:  fri  5273  dffr2  5276  frss  5278  freq1  5281  nffr  5285  frinxp  5386  frsn  5391  f1oweALT  7378  frxp  7517  frfi  8440  fpwwe2lem12  9744  fpwwe2lem13  9745  bnj1154  31385  dffr5  31960  dfon2lem9  32011  fin2so  33704  fnwe2  38118
  Copyright terms: Public domain W3C validator