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 5102
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5108 and dffr3 5533. (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 5099 . 2 wff 𝑅 Fr 𝐴
4 vx . . . . . . 7 setvar 𝑥
54cv 1522 . . . . . 6 class 𝑥
65, 1wss 3607 . . . . 5 wff 𝑥𝐴
7 c0 3948 . . . . . 6 class
85, 7wne 2823 . . . . 5 wff 𝑥 ≠ ∅
96, 8wa 383 . . . 4 wff (𝑥𝐴𝑥 ≠ ∅)
10 vz . . . . . . . . 9 setvar 𝑧
1110cv 1522 . . . . . . . 8 class 𝑧
12 vy . . . . . . . . 9 setvar 𝑦
1312cv 1522 . . . . . . . 8 class 𝑦
1411, 13, 2wbr 4685 . . . . . . 7 wff 𝑧𝑅𝑦
1514wn 3 . . . . . 6 wff ¬ 𝑧𝑅𝑦
1615, 10, 5wral 2941 . . . . 5 wff 𝑧𝑥 ¬ 𝑧𝑅𝑦
1716, 12, 5wrex 2942 . . . 4 wff 𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦
189, 17wi 4 . . 3 wff ((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
1918, 4wal 1521 . 2 wff 𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦)
203, 19wb 196 1 wff (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥𝐴𝑥 ≠ ∅) → ∃𝑦𝑥𝑧𝑥 ¬ 𝑧𝑅𝑦))
Colors of variables: wff setvar class
This definition is referenced by:  fri  5105  dffr2  5108  frss  5110  freq1  5113  nffr  5117  frinxp  5218  frsn  5223  f1oweALT  7194  frxp  7332  frfi  8246  fpwwe2lem12  9501  fpwwe2lem13  9502  bnj1154  31193  dffr5  31769  dfon2lem9  31820  fin2so  33526  fnwe2  37940
  Copyright terms: Public domain W3C validator