Metamath Proof Explorer

Theorem cvbr

Description: Binary relation expressing B covers A , which means that B is larger than A and there is nothing in between. Definition 3.2.18 of PtakPulmannova p. 68. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvbr ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ Cℋ ↔ 𝐴 ∈ Cℋ ) )
2 1 anbi1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ↔ ( 𝐴 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ) )
3 psseq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊊ 𝑧 ↔ 𝐴 ⊊ 𝑧 ) )
4 psseq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 ⊊ 𝑥 ↔ 𝐴 ⊊ 𝑥 ) )
5 4 anbi1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ↔ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ) )
6 5 rexbidv ⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ∈ Cℋ ( 𝑦 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ↔ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ) )
7 6 notbid ⊢ ( 𝑦 = 𝐴 → ( ¬ ∃ 𝑥 ∈ Cℋ ( 𝑦 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ↔ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ) )
8 3 7 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 ⊊ 𝑧 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝑦 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ) ↔ ( 𝐴 ⊊ 𝑧 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ) ) )
9 2 8 anbi12d ⊢ ( 𝑦 = 𝐴 → ( ( ( 𝑦 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ∧ ( 𝑦 ⊊ 𝑧 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝑦 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ) ) ↔ ( ( 𝐴 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ∧ ( 𝐴 ⊊ 𝑧 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ) ) ) )
10 eleq1 ⊢ ( 𝑧 = 𝐵 → ( 𝑧 ∈ Cℋ ↔ 𝐵 ∈ Cℋ ) )
11 10 anbi2d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ↔ ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ) )
12 psseq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐴 ⊊ 𝑧 ↔ 𝐴 ⊊ 𝐵 ) )
13 psseq2 ⊢ ( 𝑧 = 𝐵 → ( 𝑥 ⊊ 𝑧 ↔ 𝑥 ⊊ 𝐵 ) )
14 13 anbi2d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ↔ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
15 14 rexbidv ⊢ ( 𝑧 = 𝐵 → ( ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ↔ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
16 15 notbid ⊢ ( 𝑧 = 𝐵 → ( ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ↔ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) )
17 12 16 anbi12d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ⊊ 𝑧 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ) ↔ ( 𝐴 ⊊ 𝐵 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) ) )
18 11 17 anbi12d ⊢ ( 𝑧 = 𝐵 → ( ( ( 𝐴 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ∧ ( 𝐴 ⊊ 𝑧 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ) ) ↔ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐴 ⊊ 𝐵 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) ) ) )
19 df-cv ⊢ ⋖ℋ = { ⟨ 𝑦 , 𝑧 ⟩ ∣ ( ( 𝑦 ∈ Cℋ ∧ 𝑧 ∈ Cℋ ) ∧ ( 𝑦 ⊊ 𝑧 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝑦 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝑧 ) ) ) }
20 9 18 19 brabg ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 ↔ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ ( 𝐴 ⊊ 𝐵 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) ) ) )
21 20 bianabs ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∧ ¬ ∃ 𝑥 ∈ Cℋ ( 𝐴 ⊊ 𝑥 ∧ 𝑥 ⊊ 𝐵 ) ) ) )