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

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 ⊢ 𝐴 ∈ Cℋ
chpssat.2 ⊢ 𝐵 ∈ Cℋ
Assertion cvbr4i ( 𝐴 ⋖ℋ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∧ ∃ 𝑥 ∈ HAtoms ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) )

Proof

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