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 ( 𝐴 𝑥 ) = 𝐵 ) )