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 5514 and dffr3 5956. A class is called well-founded when the membership relation E (see df-eprel 5459) 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 5505 | . 2 wff 𝑅 Fr 𝐴 |
4 | vx | . . . . . . 7 setvar 𝑥 | |
5 | 4 | cv 1527 | . . . . . 6 class 𝑥 |
6 | 5, 1 | wss 3935 | . . . . 5 wff 𝑥 ⊆ 𝐴 |
7 | c0 4290 | . . . . . 6 class ∅ | |
8 | 5, 7 | wne 3016 | . . . . 5 wff 𝑥 ≠ ∅ |
9 | 6, 8 | wa 396 | . . . 4 wff (𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) |
10 | vz | . . . . . . . . 9 setvar 𝑧 | |
11 | 10 | cv 1527 | . . . . . . . 8 class 𝑧 |
12 | vy | . . . . . . . . 9 setvar 𝑦 | |
13 | 12 | cv 1527 | . . . . . . . 8 class 𝑦 |
14 | 11, 13, 2 | wbr 5058 | . . . . . . 7 wff 𝑧𝑅𝑦 |
15 | 14 | wn 3 | . . . . . 6 wff ¬ 𝑧𝑅𝑦 |
16 | 15, 10, 5 | wral 3138 | . . . . 5 wff ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦 |
17 | 16, 12, 5 | wrex 3139 | . . . 4 wff ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦 |
18 | 9, 17 | wi 4 | . . 3 wff ((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦) |
19 | 18, 4 | wal 1526 | . 2 wff ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦) |
20 | 3, 19 | wb 207 | 1 wff (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) |
Colors of variables: wff setvar class |
This definition is referenced by: fri 5511 dffr2 5514 frss 5516 freq1 5519 nffr 5523 frinxp 5628 frsn 5633 f1oweALT 7664 frxp 7811 frfi 8752 fpwwe2lem12 10052 fpwwe2lem13 10053 bnj1154 32169 dffr5 32887 dfon2lem9 32934 finorwe 34546 fin2so 34761 fnwe2 39533 |
Copyright terms: Public domain | W3C validator |