Metamath Proof Explorer


Theorem chrelat2i

Description: A consequence of relative atomicity. (Contributed by NM, 30-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chpssat.1 A C
chpssat.2 B C
Assertion chrelat2i ¬ A B x HAtoms x A ¬ x B

Proof

Step Hyp Ref Expression
1 chpssat.1 A C
2 chpssat.2 B C
3 nssinpss ¬ A B A B A
4 1 2 chincli A B C
5 4 1 chrelati A B A x HAtoms A B A B x A B x A
6 atelch x HAtoms x C
7 chlub A B C x C A C A B A x A A B x A
8 4 1 7 mp3an13 x C A B A x A A B x A
9 simpr A B A x A x A
10 8 9 syl6bir x C A B x A x A
11 10 adantld x C A B A B x A B x A x A
12 ssin x A x B x A B
13 12 notbii ¬ x A x B ¬ x A B
14 chnle A B C x C ¬ x A B A B A B x
15 4 14 mpan x C ¬ x A B A B A B x
16 13 15 syl5bb x C ¬ x A x B A B A B x
17 16 8 anbi12d x C ¬ x A x B A B A x A A B A B x A B x A
18 pm3.21 x B x A x A x B
19 orcom x A x B ¬ x A ¬ x A x A x B
20 pm4.55 ¬ ¬ x A x B x A x A x B ¬ x A
21 imor x A x A x B ¬ x A x A x B
22 19 20 21 3bitr4ri x A x A x B ¬ ¬ x A x B x A
23 18 22 sylib x B ¬ ¬ x A x B x A
24 23 con2i ¬ x A x B x A ¬ x B
25 24 adantrl ¬ x A x B A B A x A ¬ x B
26 17 25 syl6bir x C A B A B x A B x A ¬ x B
27 11 26 jcad x C A B A B x A B x A x A ¬ x B
28 6 27 syl x HAtoms A B A B x A B x A x A ¬ x B
29 28 reximia x HAtoms A B A B x A B x A x HAtoms x A ¬ x B
30 5 29 syl A B A x HAtoms x A ¬ x B
31 3 30 sylbi ¬ A B x HAtoms x A ¬ x B
32 sstr2 x A A B x B
33 32 com12 A B x A x B
34 33 ralrimivw A B x HAtoms x A x B
35 iman x A x B ¬ x A ¬ x B
36 35 ralbii x HAtoms x A x B x HAtoms ¬ x A ¬ x B
37 ralnex x HAtoms ¬ x A ¬ x B ¬ x HAtoms x A ¬ x B
38 36 37 bitri x HAtoms x A x B ¬ x HAtoms x A ¬ x B
39 34 38 sylib A B ¬ x HAtoms x A ¬ x B
40 39 con2i x HAtoms x A ¬ x B ¬ A B
41 31 40 impbii ¬ A B x HAtoms x A ¬ x B