| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-fr | Structured version Visualization version GIF version | ||
| Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5646 and dffr3 6117. A class is called well-founded when the membership relation E (see df-eprel 5584) 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.) |
| Ref | Expression |
|---|---|
| df-fr | ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | cR | . . 3 class 𝑅 | |
| 3 | 1, 2 | wfr 5634 | . 2 wff 𝑅 Fr 𝐴 |
| 4 | vx | . . . . . . 7 setvar 𝑥 | |
| 5 | 4 | cv 1539 | . . . . . 6 class 𝑥 |
| 6 | 5, 1 | wss 3951 | . . . . 5 wff 𝑥 ⊆ 𝐴 |
| 7 | c0 4333 | . . . . . 6 class ∅ | |
| 8 | 5, 7 | wne 2940 | . . . . 5 wff 𝑥 ≠ ∅ |
| 9 | 6, 8 | wa 395 | . . . 4 wff (𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) |
| 10 | vz | . . . . . . . . 9 setvar 𝑧 | |
| 11 | 10 | cv 1539 | . . . . . . . 8 class 𝑧 |
| 12 | vy | . . . . . . . . 9 setvar 𝑦 | |
| 13 | 12 | cv 1539 | . . . . . . . 8 class 𝑦 |
| 14 | 11, 13, 2 | wbr 5143 | . . . . . . 7 wff 𝑧𝑅𝑦 |
| 15 | 14 | wn 3 | . . . . . 6 wff ¬ 𝑧𝑅𝑦 |
| 16 | 15, 10, 5 | wral 3061 | . . . . 5 wff ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦 |
| 17 | 16, 12, 5 | wrex 3070 | . . . 4 wff ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦 |
| 18 | 9, 17 | wi 4 | . . 3 wff ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦) |
| 19 | 18, 4 | wal 1538 | . 2 wff ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦) |
| 20 | 3, 19 | wb 206 | 1 wff (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: dffr6 5640 friOLD 5643 dffr2 5646 dffr2ALT 5647 frss 5649 freq1 5652 nffr 5658 frinxp 5768 frsn 5773 f1oweALT 7997 frxp 8151 frxp2 8169 frxp3 8176 frfi 9321 fpwwe2lem11 10681 fpwwe2lem12 10682 lrrecfr 27976 bnj1154 35013 dffr5 35754 dfon2lem9 35792 weiunfr 36468 finorwe 37383 fin2so 37614 fnwe2 43065 |
| Copyright terms: Public domain | W3C validator |