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∈HAtomsA∨ℋ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∈HAtomsA∨ℋx=B
6 4 5 jca ⊢A⋖ℋB→A⊂B∧∃x∈HAtomsA∨ℋ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∈HAtomsA∨ℋx=B→A⋖ℋB
19 18 imp ⊢A⊂B∧∃x∈HAtomsA∨ℋx=B→A⋖ℋB
20 6 19 impbii ⊢A⋖ℋB↔A⊂B∧∃x∈HAtomsA∨ℋx=B