This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑝 ) 𝑏 ) ) } )