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

Metamath Proof Explorer

Theorem cvbr2

Description: Binary relation expressing B covers A . Definition of covers in Kalmbach p. 15. (Contributed by NM, 9-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion cvbr2 ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ B ↔ A ⊂ B ∧ ∀ x ∈ C ℋ A ⊂ x ∧ x ⊆ B → x = B

Proof

Step Hyp Ref Expression
1 cvbr ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ B ↔ A ⊂ B ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
2 iman ⊢ A ⊂ x ∧ x ⊆ B → x = B ↔ ¬ A ⊂ x ∧ x ⊆ B ∧ ¬ x = B
3 anass ⊢ A ⊂ x ∧ x ⊆ B ∧ ¬ x = B ↔ A ⊂ x ∧ x ⊆ B ∧ ¬ x = B
4 dfpss2 ⊢ x ⊂ B ↔ x ⊆ B ∧ ¬ x = B
5 4 anbi2i ⊢ A ⊂ x ∧ x ⊂ B ↔ A ⊂ x ∧ x ⊆ B ∧ ¬ x = B
6 3 5 bitr4i ⊢ A ⊂ x ∧ x ⊆ B ∧ ¬ x = B ↔ A ⊂ x ∧ x ⊂ B
7 2 6 xchbinx ⊢ A ⊂ x ∧ x ⊆ B → x = B ↔ ¬ A ⊂ x ∧ x ⊂ B
8 7 ralbii ⊢ ∀ x ∈ C ℋ A ⊂ x ∧ x ⊆ B → x = B ↔ ∀ x ∈ C ℋ ¬ A ⊂ x ∧ x ⊂ B
9 ralnex ⊢ ∀ x ∈ C ℋ ¬ A ⊂ x ∧ x ⊂ B ↔ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
10 8 9 bitri ⊢ ∀ x ∈ C ℋ A ⊂ x ∧ x ⊆ B → x = B ↔ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
11 10 anbi2i ⊢ A ⊂ B ∧ ∀ x ∈ C ℋ A ⊂ x ∧ x ⊆ B → x = B ↔ A ⊂ B ∧ ¬ ∃ x ∈ C ℋ A ⊂ x ∧ x ⊂ B
12 1 11 bitr4di ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ B ↔ A ⊂ B ∧ ∀ x ∈ C ℋ A ⊂ x ∧ x ⊆ B → x = B