Metamath Proof Explorer

Theorem cvbr4i

Description: An alternate way to express the covering property. (Contributed by NM, 30-Nov-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chpssat.1 ⊢ A ∈ C ℋ
chpssat.2 ⊢ B ∈ C ℋ
Assertion cvbr4i ⊢ A ⋖ ℋ B ↔ A ⊂ B ∧ ∃ x ∈ HAtoms A ∨ ℋ x = B

Proof

Step Hyp Ref Expression
1 chpssat.1 ⊢ A ∈ C ℋ
2 chpssat.2 ⊢ B ∈ C ℋ
3 cvpss ⊢ A ∈ C ℋ ∧ B ∈ C ℋ → A ⋖ ℋ B → A ⊂ B
4 1 2 3 mp2an ⊢ A ⋖ ℋ B → A ⊂ B
5 1 2 cvati ⊢ A ⋖ ℋ B → ∃ x ∈ HAtoms A ∨ ℋ x = B
6 4 5 jca ⊢ A ⋖ ℋ B → A ⊂ B ∧ ∃ x ∈ HAtoms A ∨ ℋ x = B
7 chcv2 ⊢ A ∈ C ℋ ∧ x ∈ HAtoms → A ⊂ A ∨ ℋ x ↔ A ⋖ ℋ A ∨ ℋ x
8 1 7 mpan ⊢ x ∈ HAtoms → A ⊂ A ∨ ℋ x ↔ A ⋖ ℋ A ∨ ℋ x
9 8 adantr ⊢ x ∈ HAtoms ∧ A ∨ ℋ x = B → A ⊂ A ∨ ℋ x ↔ A ⋖ ℋ A ∨ ℋ x
10 psseq2 ⊢ A ∨ ℋ x = B → A ⊂ A ∨ ℋ x ↔ A ⊂ B
11 10 adantl ⊢ x ∈ HAtoms ∧ A ∨ ℋ x = B → A ⊂ A ∨ ℋ x ↔ A ⊂ B
12 breq2 ⊢ A ∨ ℋ x = B → A ⋖ ℋ A ∨ ℋ x ↔ A ⋖ ℋ B
13 12 adantl ⊢ x ∈ HAtoms ∧ A ∨ ℋ x = B → A ⋖ ℋ A ∨ ℋ x ↔ A ⋖ ℋ B
14 9 11 13 3bitr3d ⊢ x ∈ HAtoms ∧ A ∨ ℋ x = B → A ⊂ B ↔ A ⋖ ℋ B
15 14 biimpd ⊢ x ∈ HAtoms ∧ A ∨ ℋ x = B → A ⊂ B → A ⋖ ℋ B
16 15 ex ⊢ x ∈ HAtoms → A ∨ ℋ x = B → A ⊂ B → A ⋖ ℋ B
17 16 com3r ⊢ A ⊂ B → x ∈ HAtoms → A ∨ ℋ x = B → A ⋖ ℋ B
18 17 rexlimdv ⊢ A ⊂ B → ∃ x ∈ HAtoms A ∨ ℋ x = B → A ⋖ ℋ B
19 18 imp ⊢ A ⊂ B ∧ ∃ x ∈ HAtoms A ∨ ℋ x = B → A ⋖ ℋ B
20 6 19 impbii ⊢ A ⋖ ℋ B ↔ A ⊂ B ∧ ∃ x ∈ HAtoms A ∨ ℋ x = B