This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. CH
chpssat.2 
|- B e. CH
Assertion chrelat2i 
|- ( -. A C_ B <-> E. x e. HAtoms ( x C_ A /\ -. x C_ B ) )

Proof

Step Hyp Ref Expression
1 chpssat.1 
 |-  A e. CH
2 chpssat.2 
 |-  B e. CH
3 nssinpss 
 |-  ( -. A C_ B <-> ( A i^i B ) C. A )
4 1 2 chincli 
 |-  ( A i^i B ) e. CH
5 4 1 chrelati 
 |-  ( ( A i^i B ) C. A -> E. x e. HAtoms ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ A ) )
6 atelch 
 |-  ( x e. HAtoms -> x e. CH )
7 chlub 
 |-  ( ( ( A i^i B ) e. CH /\ x e. CH /\ A e. CH ) -> ( ( ( A i^i B ) C_ A /\ x C_ A ) <-> ( ( A i^i B ) vH x ) C_ A ) )
8 4 1 7 mp3an13 
 |-  ( x e. CH -> ( ( ( A i^i B ) C_ A /\ x C_ A ) <-> ( ( A i^i B ) vH x ) C_ A ) )
9 simpr 
 |-  ( ( ( A i^i B ) C_ A /\ x C_ A ) -> x C_ A )
10 8 9 biimtrrdi 
 |-  ( x e. CH -> ( ( ( A i^i B ) vH x ) C_ A -> x C_ A ) )
11 10 adantld 
 |-  ( x e. CH -> ( ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ A ) -> x C_ A ) )
12 ssin 
 |-  ( ( x C_ A /\ x C_ B ) <-> x C_ ( A i^i B ) )
13 12 notbii 
 |-  ( -. ( x C_ A /\ x C_ B ) <-> -. x C_ ( A i^i B ) )
14 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 ) ) )
15 4 14 mpan 
 |-  ( x e. CH -> ( -. x C_ ( A i^i B ) <-> ( A i^i B ) C. ( ( A i^i B ) vH x ) ) )
16 13 15 bitrid 
 |-  ( x e. CH -> ( -. ( x C_ A /\ x C_ B ) <-> ( A i^i B ) C. ( ( A i^i B ) vH x ) ) )
17 16 8 anbi12d 
 |-  ( x e. CH -> ( ( -. ( x C_ A /\ x C_ B ) /\ ( ( A i^i B ) C_ A /\ x C_ A ) ) <-> ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ A ) ) )
18 pm3.21 
 |-  ( x C_ B -> ( x C_ A -> ( x C_ A /\ x C_ B ) ) )
19 orcom 
 |-  ( ( ( x C_ A /\ x C_ B ) \/ -. x C_ A ) <-> ( -. x C_ A \/ ( x C_ A /\ x C_ B ) ) )
20 pm4.55 
 |-  ( -. ( -. ( x C_ A /\ x C_ B ) /\ x C_ A ) <-> ( ( x C_ A /\ x C_ B ) \/ -. x C_ A ) )
21 imor 
 |-  ( ( x C_ A -> ( x C_ A /\ x C_ B ) ) <-> ( -. x C_ A \/ ( x C_ A /\ x C_ B ) ) )
22 19 20 21 3bitr4ri 
 |-  ( ( x C_ A -> ( x C_ A /\ x C_ B ) ) <-> -. ( -. ( x C_ A /\ x C_ B ) /\ x C_ A ) )
23 18 22 sylib 
 |-  ( x C_ B -> -. ( -. ( x C_ A /\ x C_ B ) /\ x C_ A ) )
24 23 con2i 
 |-  ( ( -. ( x C_ A /\ x C_ B ) /\ x C_ A ) -> -. x C_ B )
25 24 adantrl 
 |-  ( ( -. ( x C_ A /\ x C_ B ) /\ ( ( A i^i B ) C_ A /\ x C_ A ) ) -> -. x C_ B )
26 17 25 biimtrrdi 
 |-  ( x e. CH -> ( ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ A ) -> -. x C_ B ) )
27 11 26 jcad 
 |-  ( x e. CH -> ( ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ A ) -> ( x C_ A /\ -. x C_ B ) ) )
28 6 27 syl 
 |-  ( x e. HAtoms -> ( ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ A ) -> ( x C_ A /\ -. x C_ B ) ) )
29 28 reximia 
 |-  ( E. x e. HAtoms ( ( A i^i B ) C. ( ( A i^i B ) vH x ) /\ ( ( A i^i B ) vH x ) C_ A ) -> E. x e. HAtoms ( x C_ A /\ -. x C_ B ) )
30 5 29 syl 
 |-  ( ( A i^i B ) C. A -> E. x e. HAtoms ( x C_ A /\ -. x C_ B ) )
31 3 30 sylbi 
 |-  ( -. A C_ B -> E. x e. HAtoms ( x C_ A /\ -. x C_ B ) )
32 sstr2 
 |-  ( x C_ A -> ( A C_ B -> x C_ B ) )
33 32 com12 
 |-  ( A C_ B -> ( x C_ A -> x C_ B ) )
34 33 ralrimivw 
 |-  ( A C_ B -> A. x e. HAtoms ( x C_ A -> x C_ B ) )
35 iman 
 |-  ( ( x C_ A -> x C_ B ) <-> -. ( x C_ A /\ -. x C_ B ) )
36 35 ralbii 
 |-  ( A. x e. HAtoms ( x C_ A -> x C_ B ) <-> A. x e. HAtoms -. ( x C_ A /\ -. x C_ B ) )
37 ralnex 
 |-  ( A. x e. HAtoms -. ( x C_ A /\ -. x C_ B ) <-> -. E. x e. HAtoms ( x C_ A /\ -. x C_ B ) )
38 36 37 bitri 
 |-  ( A. x e. HAtoms ( x C_ A -> x C_ B ) <-> -. E. x e. HAtoms ( x C_ A /\ -. x C_ B ) )
39 34 38 sylib 
 |-  ( A C_ B -> -. E. x e. HAtoms ( x C_ A /\ -. x C_ B ) )
40 39 con2i 
 |-  ( E. x e. HAtoms ( x C_ A /\ -. x C_ B ) -> -. A C_ B )
41 31 40 impbii 
 |-  ( -. A C_ B <-> E. x e. HAtoms ( x C_ A /\ -. x C_ B ) )