![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-tap | GIF version |
Description: Tight apartness predicate. A relation 𝑅 is a tight apartness if it is irreflexive, symmetric, cotransitive, and tight. (Contributed by Jim Kingdon, 5-Feb-2025.) |
Ref | Expression |
---|---|
df-tap | ⊢ (𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cR | . . 3 class 𝑅 | |
3 | 1, 2 | wtap 7247 | . 2 wff 𝑅 TAp 𝐴 |
4 | 1, 2 | wap 7245 | . . 3 wff 𝑅 Ap 𝐴 |
5 | vx | . . . . . . . . 9 setvar 𝑥 | |
6 | 5 | cv 1352 | . . . . . . . 8 class 𝑥 |
7 | vy | . . . . . . . . 9 setvar 𝑦 | |
8 | 7 | cv 1352 | . . . . . . . 8 class 𝑦 |
9 | 6, 8, 2 | wbr 4003 | . . . . . . 7 wff 𝑥𝑅𝑦 |
10 | 9 | wn 3 | . . . . . 6 wff ¬ 𝑥𝑅𝑦 |
11 | 5, 7 | weq 1503 | . . . . . 6 wff 𝑥 = 𝑦 |
12 | 10, 11 | wi 4 | . . . . 5 wff (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦) |
13 | 12, 7, 1 | wral 2455 | . . . 4 wff ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦) |
14 | 13, 5, 1 | wral 2455 | . . 3 wff ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦) |
15 | 4, 14 | wa 104 | . 2 wff (𝑅 Ap 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦)) |
16 | 3, 15 | wb 105 | 1 wff (𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑦 → 𝑥 = 𝑦))) |
Colors of variables: wff set class |
This definition is referenced by: dftap2 7249 |
Copyright terms: Public domain | W3C validator |