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 5043
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5049 and dffr3 5467. (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 5040 . 2 wff 𝑅 Fr 𝐴
4 vx . . . . . . 7 setvar 𝑥
54cv 1479 . . . . . 6 class 𝑥
65, 1wss 3560 . . . . 5 wff 𝑥𝐴
7 c0 3897 . . . . . 6 class
85, 7wne 2790 . . . . 5 wff 𝑥 ≠ ∅
96, 8wa 384 . . . 4 wff (𝑥𝐴𝑥 ≠ ∅)
10 vz . . . . . . . . 9 setvar 𝑧
1110cv 1479 . . . . . . . 8 class 𝑧
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1479 . . . . . . . 8 class 𝑦
1411, 13, 2wbr 4623 . . . . . . 7 wff 𝑧𝑅𝑦
1514wn 3 . . . . . 6 wff ¬ 𝑧𝑅𝑦
1615, 10, 5wral 2908 . . . . 5 wff 𝑧𝑥 ¬ 𝑧𝑅𝑦
1716, 12, 5wrex 2909 . . . 4 wff 𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦
189, 17wi 4 . . 3 wff ((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
1918, 4wal 1478 . 2 wff 𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
203, 19wb 196 1 wff (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
Colors of variables: wff setvar class
This definition is referenced by:  fri  5046  dffr2  5049  frss  5051  freq1  5054  nffr  5058  frinxp  5155  frsn  5160  f1oweALT  7112  frxp  7247  frfi  8165  fpwwe2lem12  9423  fpwwe2lem13  9424  bnj1154  30828  dffr5  31404  dfon2lem9  31450  fin2so  33067  fnwe2  37142
  Copyright terms: Public domain W3C validator