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 C
chpssat.2 B C
Assertion cvexchlem A B B A A B

Proof

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