Theorem chrelat2

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

	Ref	Expression
Assertion	chrelat2	|- ( ( A e. CH /\ B e. CH ) -> ( -. A C_ B <-> E. x e. HAtoms ( x C_ A /\ -. x C_ B ) ) )

Proof

Step	Hyp	Ref	Expression
1		sseq1	|- ( A = if ( A e. CH , A , ~H ) -> ( A C_ B <-> if ( A e. CH , A , ~H ) C_ B ) )
2	1	notbid	|- ( A = if ( A e. CH , A , ~H ) -> ( -. A C_ B <-> -. if ( A e. CH , A , ~H ) C_ B ) )
3		sseq2	|- ( A = if ( A e. CH , A , ~H ) -> ( x C_ A <-> x C_ if ( A e. CH , A , ~H ) ) )
4	3	anbi1d	|- ( A = if ( A e. CH , A , ~H ) -> ( ( x C_ A /\ -. x C_ B ) <-> ( x C_ if ( A e. CH , A , ~H ) /\ -. x C_ B ) ) )
5	4	rexbidv	|- ( A = if ( A e. CH , A , ~H ) -> ( E. x e. HAtoms ( x C_ A /\ -. x C_ B ) <-> E. x e. HAtoms ( x C_ if ( A e. CH , A , ~H ) /\ -. x C_ B ) ) )
6	2 5	bibi12d	|- ( A = if ( A e. CH , A , ~H ) -> ( ( -. A C_ B <-> E. x e. HAtoms ( x C_ A /\ -. x C_ B ) ) <-> ( -. if ( A e. CH , A , ~H ) C_ B <-> E. x e. HAtoms ( x C_ if ( A e. CH , A , ~H ) /\ -. x C_ B ) ) ) )
7		sseq2	|- ( B = if ( B e. CH , B , ~H ) -> ( if ( A e. CH , A , ~H ) C_ B <-> if ( A e. CH , A , ~H ) C_ if ( B e. CH , B , ~H ) ) )
8	7	notbid	|- ( B = if ( B e. CH , B , ~H ) -> ( -. if ( A e. CH , A , ~H ) C_ B <-> -. if ( A e. CH , A , ~H ) C_ if ( B e. CH , B , ~H ) ) )
9		sseq2	|- ( B = if ( B e. CH , B , ~H ) -> ( x C_ B <-> x C_ if ( B e. CH , B , ~H ) ) )
10	9	notbid	|- ( B = if ( B e. CH , B , ~H ) -> ( -. x C_ B <-> -. x C_ if ( B e. CH , B , ~H ) ) )
11	10	anbi2d	|- ( B = if ( B e. CH , B , ~H ) -> ( ( x C_ if ( A e. CH , A , ~H ) /\ -. x C_ B ) <-> ( x C_ if ( A e. CH , A , ~H ) /\ -. x C_ if ( B e. CH , B , ~H ) ) ) )
12	11	rexbidv	|- ( B = if ( B e. CH , B , ~H ) -> ( E. x e. HAtoms ( x C_ if ( A e. CH , A , ~H ) /\ -. x C_ B ) <-> E. x e. HAtoms ( x C_ if ( A e. CH , A , ~H ) /\ -. x C_ if ( B e. CH , B , ~H ) ) ) )
13	8 12	bibi12d	|- ( B = if ( B e. CH , B , ~H ) -> ( ( -. if ( A e. CH , A , ~H ) C_ B <-> E. x e. HAtoms ( x C_ if ( A e. CH , A , ~H ) /\ -. x C_ B ) ) <-> ( -. if ( A e. CH , A , ~H ) C_ if ( B e. CH , B , ~H ) <-> E. x e. HAtoms ( x C_ if ( A e. CH , A , ~H ) /\ -. x C_ if ( B e. CH , B , ~H ) ) ) ) )
14		ifchhv	|- if ( A e. CH , A , ~H ) e. CH
15		ifchhv	|- if ( B e. CH , B , ~H ) e. CH
16	14 15	chrelat2i	|- ( -. if ( A e. CH , A , ~H ) C_ if ( B e. CH , B , ~H ) <-> E. x e. HAtoms ( x C_ if ( A e. CH , A , ~H ) /\ -. x C_ if ( B e. CH , B , ~H ) ) )
17	6 13 16	dedth2h	|- ( ( A e. CH /\ B e. CH ) -> ( -. A C_ B <-> E. x e. HAtoms ( x C_ A /\ -. x C_ B ) ) )