Definition df-covers

Description: Define the covers relation ("is covered by") for posets. " a is covered by b " means that a is strictly less than b and there is nothing in between. See cvrval for the relation form. (Contributed by NM, 18-Sep-2011)

	Ref	Expression
Assertion	df-covers	⊢ ⋖ = ( 𝑝 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑝 ) ∧ 𝑏 ∈ ( Base ‘ 𝑝 ) ) ∧ 𝑎 ( lt ‘ 𝑝 ) 𝑏 ∧ ¬ ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑎 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑏 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccvr	⊢ ⋖
1		vp	⊢ 𝑝
2		cvv	⊢ V
3		va	⊢ 𝑎
4		vb	⊢ 𝑏
5	3	cv	⊢ 𝑎
6		cbs	⊢ Base
7	1	cv	⊢ 𝑝
8	7 6	cfv	⊢ ( Base ‘ 𝑝 )
9	5 8	wcel	⊢ 𝑎 ∈ ( Base ‘ 𝑝 )
10	4	cv	⊢ 𝑏
11	10 8	wcel	⊢ 𝑏 ∈ ( Base ‘ 𝑝 )
12	9 11	wa	⊢ ( 𝑎 ∈ ( Base ‘ 𝑝 ) ∧ 𝑏 ∈ ( Base ‘ 𝑝 ) )
13		cplt	⊢ lt
14	7 13	cfv	⊢ ( lt ‘ 𝑝 )
15	5 10 14	wbr	⊢ 𝑎 ( lt ‘ 𝑝 ) 𝑏
16		vz	⊢ 𝑧
17	16	cv	⊢ 𝑧
18	5 17 14	wbr	⊢ 𝑎 ( lt ‘ 𝑝 ) 𝑧
19	17 10 14	wbr	⊢ 𝑧 ( lt ‘ 𝑝 ) 𝑏
20	18 19	wa	⊢ ( 𝑎 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑏 )
21	20 16 8	wrex	⊢ ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑎 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑏 )
22	21	wn	⊢ ¬ ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑎 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑏 )
23	12 15 22	w3a	⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑝 ) ∧ 𝑏 ∈ ( Base ‘ 𝑝 ) ) ∧ 𝑎 ( lt ‘ 𝑝 ) 𝑏 ∧ ¬ ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑎 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑏 ) )
24	23 3 4	copab	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑝 ) ∧ 𝑏 ∈ ( Base ‘ 𝑝 ) ) ∧ 𝑎 ( lt ‘ 𝑝 ) 𝑏 ∧ ¬ ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑎 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑏 ) ) }
25	1 2 24	cmpt	⊢ ( 𝑝 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑝 ) ∧ 𝑏 ∈ ( Base ‘ 𝑝 ) ) ∧ 𝑎 ( lt ‘ 𝑝 ) 𝑏 ∧ ¬ ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑎 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑏 ) ) } )
26	0 25	wceq	⊢ ⋖ = ( 𝑝 ∈ V ↦ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( Base ‘ 𝑝 ) ∧ 𝑏 ∈ ( Base ‘ 𝑝 ) ) ∧ 𝑎 ( lt ‘ 𝑝 ) 𝑏 ∧ ¬ ∃ 𝑧 ∈ ( Base ‘ 𝑝 ) ( 𝑎 ( lt ‘ 𝑝 ) 𝑧 ∧ 𝑧 ( lt ‘ 𝑝 ) 𝑏 ) ) } )