Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-covers Structured version   Visualization version   GIF version

Definition df-covers 33370
Description: Define the covers relation ("is covered by") for posets. "𝑎 is covered by 𝑏 " means that 𝑎 is strictly less than 𝑏 and there is nothing in between. See cvrval 33373 for the relation form. (Contributed by NM, 18-Sep-2011.)
Assertion
Ref Expression
df-covers ⋖ = (𝑝 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏))})
Distinct variable group:   𝑧,𝑝,𝑎,𝑏

Detailed syntax breakdown of Definition df-covers
StepHypRef Expression
1 ccvr 33366 . 2 class
2 vp . . 3 setvar 𝑝
3 cvv 3168 . . 3 class V
4 va . . . . . . . 8 setvar 𝑎
54cv 1473 . . . . . . 7 class 𝑎
62cv 1473 . . . . . . . 8 class 𝑝
7 cbs 15637 . . . . . . . 8 class Base
86, 7cfv 5786 . . . . . . 7 class (Base‘𝑝)
95, 8wcel 1975 . . . . . 6 wff 𝑎 ∈ (Base‘𝑝)
10 vb . . . . . . . 8 setvar 𝑏
1110cv 1473 . . . . . . 7 class 𝑏
1211, 8wcel 1975 . . . . . 6 wff 𝑏 ∈ (Base‘𝑝)
139, 12wa 382 . . . . 5 wff (𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝))
14 cplt 16706 . . . . . . 7 class lt
156, 14cfv 5786 . . . . . 6 class (lt‘𝑝)
165, 11, 15wbr 4573 . . . . 5 wff 𝑎(lt‘𝑝)𝑏
17 vz . . . . . . . . . 10 setvar 𝑧
1817cv 1473 . . . . . . . . 9 class 𝑧
195, 18, 15wbr 4573 . . . . . . . 8 wff 𝑎(lt‘𝑝)𝑧
2018, 11, 15wbr 4573 . . . . . . . 8 wff 𝑧(lt‘𝑝)𝑏
2119, 20wa 382 . . . . . . 7 wff (𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏)
2221, 17, 8wrex 2892 . . . . . 6 wff 𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏)
2322wn 3 . . . . 5 wff ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏)
2413, 16, 23w3a 1030 . . . 4 wff ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏))
2524, 4, 10copab 4632 . . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏))}
262, 3, 25cmpt 4633 . 2 class (𝑝 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏))})
271, 26wceq 1474 1 wff ⋖ = (𝑝 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏))})
Colors of variables: wff setvar class
This definition is referenced by:  cvrfval  33372
  Copyright terms: Public domain W3C validator