Metamath Proof Explorer

Theorem cvexchlem

Description: Lemma for cvexchi . (Contributed by NM, 10-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chpssat.1 ⊢ 𝐴 ∈ Cℋ
chpssat.2 ⊢ 𝐵 ∈ Cℋ
Assertion cvexchlem ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 chpssat.1 ⊢ 𝐴 ∈ Cℋ
2 chpssat.2 ⊢ 𝐵 ∈ Cℋ
3 1 2 chincli ⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
4 cvpss ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) )
5 3 2 4 mp2an ⊢ ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 )
6 3 2 chpssati ⊢ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) )
7 5 6 syl ⊢ ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) )
8 ssin ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) )
9 ancom ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ) )
10 8 9 bitr3i ⊢ ( 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ) )
11 10 baibr ⊢ ( 𝑥 ⊆ 𝐵 → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) )
12 11 notbid ⊢ ( 𝑥 ⊆ 𝐵 → ( ¬ 𝑥 ⊆ 𝐴 ↔ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) )
13 12 biimpar ⊢ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) → ¬ 𝑥 ⊆ 𝐴 )
14 chcv1 ⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ HAtoms ) → ( ¬ 𝑥 ⊆ 𝐴 ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ) )
15 1 14 mpan ⊢ ( 𝑥 ∈ HAtoms → ( ¬ 𝑥 ⊆ 𝐴 ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ) )
16 15 biimpa ⊢ ( ( 𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ 𝐴 ) → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) )
17 13 16 sylan2 ⊢ ( ( 𝑥 ∈ HAtoms ∧ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ) → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) )
18 17 adantrr ⊢ ( ( 𝑥 ∈ HAtoms ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) )
19 atelch ⊢ ( 𝑥 ∈ HAtoms → 𝑥 ∈ Cℋ )
20 1 2 chabs1i ⊢ ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = 𝐴
21 20 oveq1i ⊢ ( ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ 𝑥 )
22 chjass ⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) )
23 1 3 22 mp3an12 ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) )
24 21 23 syl5reqr ⊢ ( 𝑥 ∈ Cℋ → ( 𝐴 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) = ( 𝐴 ∨ℋ 𝑥 ) )
25 24 adantr ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → ( 𝐴 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) = ( 𝐴 ∨ℋ 𝑥 ) )
26 ancom ⊢ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ 𝑥 ⊆ 𝐵 ) )
27 chnle ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) )
28 3 27 mpan ⊢ ( 𝑥 ∈ Cℋ → ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) )
29 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
30 29 biantrur ⊢ ( 𝑥 ⊆ 𝐵 ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) )
31 chlub ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) )
32 3 2 31 mp3an13 ⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) )
33 30 32 syl5bb ⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ 𝐵 ↔ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) )
34 28 33 anbi12d ⊢ ( 𝑥 ∈ Cℋ → ( ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) )
35 26 34 syl5bb ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) )
36 chjcl ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∈ Cℋ )
37 3 36 mpan ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∈ Cℋ )
38 cvnbtwn2 ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 ) ) )
39 3 2 38 mp3an12 ⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∈ Cℋ → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 ) ) )
40 37 39 syl ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 ) ) )
41 40 com23 ⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 ) ) )
42 35 41 sylbid ⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 ) ) )
43 42 imp32 ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 )
44 43 oveq2d ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → ( 𝐴 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) = ( 𝐴 ∨ℋ 𝐵 ) )
45 25 44 eqtr3d ⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → ( 𝐴 ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ 𝐵 ) )
46 19 45 sylan ⊢ ( ( 𝑥 ∈ HAtoms ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → ( 𝐴 ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ 𝐵 ) )
47 18 46 breqtrd ⊢ ( ( 𝑥 ∈ HAtoms ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) )
48 47 exp32 ⊢ ( 𝑥 ∈ HAtoms → ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) )
49 48 rexlimiv ⊢ ( ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) )
50 7 49 mpcom ⊢ ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) )