Definition df-covers 39267

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 39270 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 39263	. 2 class ⋖
2		vp	. . 3 setvar 𝑝
3		cvv 3480	. . 3 class V
4		va	. . . . . . . 8 setvar 𝑎
5	4	cv 1539	. . . . . . 7 class 𝑎
6	2	cv 1539	. . . . . . . 8 class 𝑝
7		cbs 17247	. . . . . . . 8 class Base
8	6, 7	cfv 6561	. . . . . . 7 class (Base‘𝑝)
9	5, 8	wcel 2108	. . . . . 6 wff 𝑎 ∈ (Base‘𝑝)
10		vb	. . . . . . . 8 setvar 𝑏
11	10	cv 1539	. . . . . . 7 class 𝑏
12	11, 8	wcel 2108	. . . . . 6 wff 𝑏 ∈ (Base‘𝑝)
13	9, 12	wa 395	. . . . 5 wff (𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝))
14		cplt 18354	. . . . . . 7 class lt
15	6, 14	cfv 6561	. . . . . 6 class (lt‘𝑝)
16	5, 11, 15	wbr 5143	. . . . 5 wff 𝑎(lt‘𝑝)𝑏
17		vz	. . . . . . . . . 10 setvar 𝑧
18	17	cv 1539	. . . . . . . . 9 class 𝑧
19	5, 18, 15	wbr 5143	. . . . . . . 8 wff 𝑎(lt‘𝑝)𝑧
20	18, 11, 15	wbr 5143	. . . . . . . 8 wff 𝑧(lt‘𝑝)𝑏
21	19, 20	wa 395	. . . . . . 7 wff (𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏)
22	21, 17, 8	wrex 3070	. . . . . 6 wff ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏)
23	22	wn 3	. . . . 5 wff ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏)
24	13, 16, 23	w3a 1087	. . . 4 wff ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))
25	24, 4, 10	copab 5205	. . 3 class {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))}
26	2, 3, 25	cmpt 5225	. 2 class (𝑝 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))})
27	1, 26	wceq 1540	1 wff ⋖ = (𝑝 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))})

This definition is referenced by:  cvrfval  39269