ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-tap GIF version

Definition df-tap 7248
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.)
Assertion
Ref Expression
df-tap (𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝑅,𝑦

Detailed syntax breakdown of Definition df-tap
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wtap 7247 . 2 wff 𝑅 TAp 𝐴
41, 2wap 7245 . . 3 wff 𝑅 Ap 𝐴
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1352 . . . . . . . 8 class 𝑥
7 vy . . . . . . . . 9 setvar 𝑦
87cv 1352 . . . . . . . 8 class 𝑦
96, 8, 2wbr 4003 . . . . . . 7 wff 𝑥𝑅𝑦
109wn 3 . . . . . 6 wff ¬ 𝑥𝑅𝑦
115, 7weq 1503 . . . . . 6 wff 𝑥 = 𝑦
1210, 11wi 4 . . . . 5 wff 𝑥𝑅𝑦𝑥 = 𝑦)
1312, 7, 1wral 2455 . . . 4 wff 𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦)
1413, 5, 1wral 2455 . . 3 wff 𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦)
154, 14wa 104 . 2 wff (𝑅 Ap 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦))
163, 15wb 105 1 wff (𝑅 TAp 𝐴 ↔ (𝑅 Ap 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑥𝑅𝑦𝑥 = 𝑦)))
Colors of variables: wff set class
This definition is referenced by:  dftap2  7249
  Copyright terms: Public domain W3C validator