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 chjass ( ( 𝐴C ∧ ( 𝐴𝐵 ) ∈ C𝑥C ) → ( ( 𝐴 ( 𝐴𝐵 ) ) ∨ 𝑥 ) = ( 𝐴 ( ( 𝐴𝐵 ) ∨ 𝑥 ) ) )
21 1 3 20 mp3an12 ( 𝑥C → ( ( 𝐴 ( 𝐴𝐵 ) ) ∨ 𝑥 ) = ( 𝐴 ( ( 𝐴𝐵 ) ∨ 𝑥 ) ) )
22 1 2 chabs1i ( 𝐴 ( 𝐴𝐵 ) ) = 𝐴
23 22 oveq1i ( ( 𝐴 ( 𝐴𝐵 ) ) ∨ 𝑥 ) = ( 𝐴 𝑥 )
24 21 23 eqtr3di ( 𝑥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 ( ( 𝐴𝐵 ) ⋖ 𝐵𝐴 ( 𝐴 𝐵 ) )