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	syl6bir	|- ( 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	syl5bb	|- ( 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	syl6bir	|- ( 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 ) )