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 34379
 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 34382 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 34375 . 2 class
2 vp . . 3 setvar 𝑝
3 cvv 3198 . . 3 class V
4 va . . . . . . . 8 setvar 𝑎
54cv 1481 . . . . . . 7 class 𝑎
62cv 1481 . . . . . . . 8 class 𝑝
7 cbs 15851 . . . . . . . 8 class Base
86, 7cfv 5886 . . . . . . 7 class (Base‘𝑝)
95, 8wcel 1989 . . . . . 6 wff 𝑎 ∈ (Base‘𝑝)
10 vb . . . . . . . 8 setvar 𝑏
1110cv 1481 . . . . . . 7 class 𝑏
1211, 8wcel 1989 . . . . . 6 wff 𝑏 ∈ (Base‘𝑝)
139, 12wa 384 . . . . 5 wff (𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝))
14 cplt 16935 . . . . . . 7 class lt
156, 14cfv 5886 . . . . . 6 class (lt‘𝑝)
165, 11, 15wbr 4651 . . . . 5 wff 𝑎(lt‘𝑝)𝑏
17 vz . . . . . . . . . 10 setvar 𝑧
1817cv 1481 . . . . . . . . 9 class 𝑧
195, 18, 15wbr 4651 . . . . . . . 8 wff 𝑎(lt‘𝑝)𝑧
2018, 11, 15wbr 4651 . . . . . . . 8 wff 𝑧(lt‘𝑝)𝑏
2119, 20wa 384 . . . . . . 7 wff (𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏)
2221, 17, 8wrex 2912 . . . . . 6 wff 𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏)
2322wn 3 . . . . 5 wff ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏)
2413, 16, 23w3a 1037 . . . 4 wff ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏))
2524, 4, 10copab 4710 . . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏))}
262, 3, 25cmpt 4727 . 2 class (𝑝 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏))})
271, 26wceq 1482 1 wff ⋖ = (𝑝 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧𝑧(lt‘𝑝)𝑏))})
 Colors of variables: wff setvar class This definition is referenced by:  cvrfval  34381
 Copyright terms: Public domain W3C validator