Definition df-covers 33571

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 33574 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

Step	Hyp	Ref	Expression
1		ccvr 33567	. 2 class ⋖
2		vp	. . 3 setvar 𝑝
3		cvv 3173	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1474	. . . . . . 7 class 𝑎
6	2	cv 1474	. . . . . . . 8 class 𝑝
7		cbs 15695	. . . . . . . 8 class Base
8	6, 7	cfv 5804	. . . . . . 7 class (Base‘𝑝)
9	5, 8	wcel 1977	. . . . . 6 wff 𝑎 ∈ (Base‘𝑝)
10		vb	. . . . . . . 8 setvar 𝑏
11	10	cv 1474	. . . . . . 7 class 𝑏
12	11, 8	wcel 1977	. . . . . 6 wff 𝑏 ∈ (Base‘𝑝)
13	9, 12	wa 383	. . . . 5 wff (𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝))
14		cplt 16764	. . . . . . 7 class lt
15	6, 14	cfv 5804	. . . . . 6 class (lt‘𝑝)
16	5, 11, 15	wbr 4583	. . . . 5 wff 𝑎(lt‘𝑝)𝑏
17		vz	. . . . . . . . . 10 setvar 𝑧
18	17	cv 1474	. . . . . . . . 9 class 𝑧
19	5, 18, 15	wbr 4583	. . . . . . . 8 wff 𝑎(lt‘𝑝)𝑧
20	18, 11, 15	wbr 4583	. . . . . . . 8 wff 𝑧(lt‘𝑝)𝑏
21	19, 20	wa 383	. . . . . . 7 wff (𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏)
22	21, 17, 8	wrex 2897	. . . . . 6 wff ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏)
23	22	wn 3	. . . . 5 wff ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏)
24	13, 16, 23	w3a 1031	. . . 4 wff ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))
25	24, 4, 10	copab 4642	. . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))}
26	2, 3, 25	cmpt 4643	. 2 class (𝑝 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))})
27	1, 26	wceq 1475	1 wff ⋖ = (𝑝 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))})

This definition is referenced by:  cvrfval  33573