Metamath Proof Explorer

Theorem cvexchlem

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

Ref Expression
Hypotheses chpssat.1 
|- A e. CH
chpssat.2 
|- B e. CH
Assertion cvexchlem 
|- ( ( A i^i B )  A

Proof

Step Hyp Ref Expression
1 chpssat.1 
 |-  A e. CH
2 chpssat.2 
 |-  B e. CH
3 1 2 chincli 
 |-  ( A i^i B ) e. CH
4 cvpss 
 |-  ( ( ( A i^i B ) e. CH /\ B e. CH ) -> ( ( A i^i B )  ( A i^i B ) C. B ) )
5 3 2 4 mp2an 
 |-  ( ( A i^i B )  ( A i^i B ) C. B )
6 3 2 chpssati 
 |-  ( ( A i^i B ) C. B -> E. x e. HAtoms ( x C_ B /\ -. x C_ ( A i^i B ) ) )
7 5 6 syl 
 |-  ( ( A i^i B )  E. x e. HAtoms ( x C_ B /\ -. x C_ ( A i^i B ) ) )
8 ssin 
 |-  ( ( x C_ A /\ x C_ B ) <-> x C_ ( A i^i B ) )
9 ancom 
 |-  ( ( x C_ A /\ x C_ B ) <-> ( x C_ B /\ x C_ A ) )
10 8 9 bitr3i 
 |-  ( x C_ ( A i^i B ) <-> ( x C_ B /\ x C_ A ) )
11 10 baibr 
 |-  ( x C_ B -> ( x C_ A <-> x C_ ( A i^i B ) ) )
12 11 notbid 
 |-  ( x C_ B -> ( -. x C_ A <-> -. x C_ ( A i^i B ) ) )
13 12 biimpar 
 |-  ( ( x C_ B /\ -. x C_ ( A i^i B ) ) -> -. x C_ A )
14 chcv1 
 |-  ( ( A e. CH /\ x e. HAtoms ) -> ( -. x C_ A <-> A
15 1 14 mpan 
 |-  ( x e. HAtoms -> ( -. x C_ A <-> A
16 15 biimpa 
 |-  ( ( x e. HAtoms /\ -. x C_ A ) -> A
17 13 16 sylan2 
 |-  ( ( x e. HAtoms /\ ( x C_ B /\ -. x C_ ( A i^i B ) ) ) -> A
18 17 adantrr 
 |-  ( ( x e. HAtoms /\ ( ( x C_ B /\ -. x C_ ( A i^i B ) ) /\ ( A i^i B )  A
19 atelch 
 |-  ( x e. HAtoms -> x e. CH )
20 chjass 
 |-  ( ( A e. CH /\ ( A i^i B ) e. CH /\ x e. CH ) -> ( ( A vH ( A i^i B ) ) vH x ) = ( A vH ( ( A i^i B ) vH x ) ) )
21 1 3 20 mp3an12 
 |-  ( x e. CH -> ( ( A vH ( A i^i B ) ) vH x ) = ( A vH ( ( A i^i B ) vH x ) ) )
22 1 2 chabs1i 
 |-  ( A vH ( A i^i B ) ) = A
23 22 oveq1i 
 |-  ( ( A vH ( A i^i B ) ) vH x ) = ( A vH x )
24 21 23 eqtr3di 
 |-  ( x e. CH -> ( A vH ( ( A i^i B ) vH x ) ) = ( A vH x ) )
25 24 adantr 
 |-  ( ( x e. CH /\ ( ( x C_ B /\ -. x C_ ( A i^i B ) ) /\ ( A i^i B )  ( A vH ( ( A i^i B ) vH x ) ) = ( A vH x ) )
26 ancom 
 |-  ( ( x C_ B /\ -. x C_ ( A i^i B ) ) <-> ( -. x C_ ( A i^i B ) /\ x C_ B ) )
27 chnle 
 |-  ( ( ( A i^i B ) e. CH /\ x e. CH ) -> ( -. x C_ ( A i^i B ) <-> ( A i^i B ) C. ( ( A i^i B ) vH x ) ) )
28 3 27 mpan 
 |-  ( x e. CH -> ( -. x C_ ( A i^i B ) <-> ( A i^i B ) C. ( ( A i^i B ) vH x ) ) )
29 inss2 
 |-  ( A i^i B ) C_ B
30 29 biantrur 
 |-  ( x C_ B <-> ( ( A i^i B ) C_ B /\ x C_ B ) )
31 chlub 
 |-  ( ( ( A i^i B ) e. CH /\ x e. CH /\ B e. CH ) -> ( ( ( A i^i B ) C_ B /\ x C_ B ) <-> ( ( A i^i B ) vH x ) C_ B ) )
32 3 2 31 mp3an13 
 |-  ( x e. CH -> ( ( ( A i^i B ) C_ B /\ x C_ B ) <-> ( ( A i^i B ) vH x ) C_ B ) )
33 30 32 bitrid 
 |-  ( x e. CH -> ( x C_ B <-> ( ( A i^i B ) vH x ) C_ B ) )
34 28 33 anbi12d 
 |-  ( x e. CH -> ( ( -. x C_ ( A i^i B ) /\ x C_ B ) <-> ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ B ) ) )
35 26 34 bitrid 
 |-  ( x e. CH -> ( ( x C_ B /\ -. x C_ ( A i^i B ) ) <-> ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ B ) ) )
36 chjcl 
 |-  ( ( ( A i^i B ) e. CH /\ x e. CH ) -> ( ( A i^i B ) vH x ) e. CH )
37 3 36 mpan 
 |-  ( x e. CH -> ( ( A i^i B ) vH x ) e. CH )
38 cvnbtwn2 
 |-  ( ( ( A i^i B ) e. CH /\ B e. CH /\ ( ( A i^i B ) vH x ) e. CH ) -> ( ( A i^i B )  ( ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ B ) -> ( ( A i^i B ) vH x ) = B ) ) )
39 3 2 38 mp3an12 
 |-  ( ( ( A i^i B ) vH x ) e. CH -> ( ( A i^i B )  ( ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ B ) -> ( ( A i^i B ) vH x ) = B ) ) )
40 37 39 syl 
 |-  ( x e. CH -> ( ( A i^i B )  ( ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ B ) -> ( ( A i^i B ) vH x ) = B ) ) )
41 40 com23 
 |-  ( x e. CH -> ( ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ B ) -> ( ( A i^i B )  ( ( A i^i B ) vH x ) = B ) ) )
42 35 41 sylbid 
 |-  ( x e. CH -> ( ( x C_ B /\ -. x C_ ( A i^i B ) ) -> ( ( A i^i B )  ( ( A i^i B ) vH x ) = B ) ) )
43 42 imp32 
 |-  ( ( x e. CH /\ ( ( x C_ B /\ -. x C_ ( A i^i B ) ) /\ ( A i^i B )  ( ( A i^i B ) vH x ) = B )
44 43 oveq2d 
 |-  ( ( x e. CH /\ ( ( x C_ B /\ -. x C_ ( A i^i B ) ) /\ ( A i^i B )  ( A vH ( ( A i^i B ) vH x ) ) = ( A vH B ) )
45 25 44 eqtr3d 
 |-  ( ( x e. CH /\ ( ( x C_ B /\ -. x C_ ( A i^i B ) ) /\ ( A i^i B )  ( A vH x ) = ( A vH B ) )
46 19 45 sylan 
 |-  ( ( x e. HAtoms /\ ( ( x C_ B /\ -. x C_ ( A i^i B ) ) /\ ( A i^i B )  ( A vH x ) = ( A vH B ) )
47 18 46 breqtrd 
 |-  ( ( x e. HAtoms /\ ( ( x C_ B /\ -. x C_ ( A i^i B ) ) /\ ( A i^i B )  A
48 47 exp32 
 |-  ( x e. HAtoms -> ( ( x C_ B /\ -. x C_ ( A i^i B ) ) -> ( ( A i^i B )  A
49 48 rexlimiv 
 |-  ( E. x e. HAtoms ( x C_ B /\ -. x C_ ( A i^i B ) ) -> ( ( A i^i B )  A
50 7 49 mpcom 
 |-  ( ( A i^i B )  A