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 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ B ↔ A ⊂ B ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ y = A → y ∈ C ℋ ↔ A ∈ C ℋ
2 1 anbi1d ⊢ y = A → y ∈ C ℋ ∧ z ∈ C ℋ ↔ A ∈ C ℋ ∧ z ∈ C ℋ
3 psseq1 ⊢ y = A → y ⊂ z ↔ A ⊂ z
4 psseq1 ⊢ y = A → y ⊂ x ↔ A ⊂ x
5 4 anbi1d ⊢ y = A → y ⊂ x ∧ x ⊂ z ↔ A ⊂ x ∧ x ⊂ z
6 5 rexbidv ⊢ y = A → ∃ x ∈ C ℋ y ⊂ x ∧ x ⊂ z ↔ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ z
7 6 notbid ⊢ y = A → ¬ ∃ x ∈ C ℋ y ⊂ x ∧ x ⊂ z ↔ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ z
8 3 7 anbi12d ⊢ y = A → y ⊂ z ∧ ¬ ∃ x ∈ C ℋ y ⊂ x ∧ x ⊂ z ↔ A ⊂ z ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ z
9 2 8 anbi12d ⊢ y = A → y ∈ C ℋ ∧ z ∈ C ℋ ∧ y ⊂ z ∧ ¬ ∃ x ∈ C ℋ y ⊂ x ∧ x ⊂ z ↔ A ∈ C ℋ ∧ z ∈ C ℋ ∧ A ⊂ z ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ z
10 eleq1 ⊢ z = B → z ∈ C ℋ ↔ B ∈ C ℋ
11 10 anbi2d ⊢ z = B → A ∈ C ℋ ∧ z ∈ C ℋ ↔ A ∈ C ℋ ∧ B ∈ C ℋ
12 psseq2 ⊢ z = B → A ⊂ z ↔ A ⊂ B
13 psseq2 ⊢ z = B → x ⊂ z ↔ x ⊂ B
14 13 anbi2d ⊢ z = B → A ⊂ x ∧ x ⊂ z ↔ A ⊂ x ∧ x ⊂ B
15 14 rexbidv ⊢ z = B → ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ z ↔ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
16 15 notbid ⊢ z = B → ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ z ↔ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
17 12 16 anbi12d ⊢ z = B → A ⊂ z ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ z ↔ A ⊂ B ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
18 11 17 anbi12d ⊢ z = B → A ∈ C ℋ ∧ z ∈ C ℋ ∧ A ⊂ z ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ z ↔ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊂ B ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
19 df-cv ⊢ ⋖ ℋ = y z | y ∈ C ℋ ∧ z ∈ C ℋ ∧ y ⊂ z ∧ ¬ ∃ x ∈ C ℋ y ⊂ x ∧ x ⊂ z
20 9 18 19 brabg ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ B ↔ A ∈ C ℋ ∧ B ∈ C ℋ ∧ A ⊂ B ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
21 20 bianabs ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ B ↔ A ⊂ B ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B