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 4986
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4992 and dffr3 5403. (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 4983 . 2 wff 𝑅 Fr 𝐴
4 vx . . . . . . 7 setvar 𝑥
54cv 1473 . . . . . 6 class 𝑥
65, 1wss 3539 . . . . 5 wff 𝑥𝐴
7 c0 3873 . . . . . 6 class
85, 7wne 2779 . . . . 5 wff 𝑥 ≠ ∅
96, 8wa 382 . . . 4 wff (𝑥𝐴𝑥 ≠ ∅)
10 vz . . . . . . . . 9 setvar 𝑧
1110cv 1473 . . . . . . . 8 class 𝑧
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1473 . . . . . . . 8 class 𝑦
1411, 13, 2wbr 4577 . . . . . . 7 wff 𝑧𝑅𝑦
1514wn 3 . . . . . 6 wff ¬ 𝑧𝑅𝑦
1615, 10, 5wral 2895 . . . . 5 wff 𝑧𝑥 ¬ 𝑧𝑅𝑦
1716, 12, 5wrex 2896 . . . 4 wff 𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦
189, 17wi 4 . . 3 wff ((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
1918, 4wal 1472 . 2 wff 𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
203, 19wb 194 1 wff (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
Colors of variables: wff setvar class
This definition is referenced by:  fri  4989  dffr2  4992  frss  4994  freq1  4997  nffr  5001  frinxp  5096  frsn  5101  f1oweALT  7020  frxp  7151  frfi  8067  fpwwe2lem12  9319  fpwwe2lem13  9320  bnj1154  30114  dffr5  30689  dfon2lem9  30733  fin2so  32349  fnwe2  36424
  Copyright terms: Public domain W3C validator