chrelat2i

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

	Ref	Expression
Hypotheses	chpssat.1	$⊢ A \in C_{ℋ}$
	chpssat.2	$⊢ B \in C_{ℋ}$
Assertion	chrelat2i	$⊢ \neg A \subseteq B \leftrightarrow \exists x \in HAtoms (x \subseteq A \land \neg x \subseteq B)$

Proof

Step	Hyp	Ref	Expression
1		chpssat.1	$⊢ A \in C_{ℋ}$
2		chpssat.2	$⊢ B \in C_{ℋ}$
3		nssinpss	$⊢ \neg A \subseteq B \leftrightarrow A \cap B \subset A$
4	1 2	chincli	$⊢ A \cap B \in C_{ℋ}$
5	4 1	chrelati	$⊢ A \cap B \subset A \to \exists x \in HAtoms (A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq A)$
6		atelch	$⊢ x \in HAtoms \to x \in C_{ℋ}$
7		chlub	$⊢ (A \cap B \in C_{ℋ} \land x \in C_{ℋ} \land A \in C_{ℋ}) \to ((A \cap B \subseteq A \land x \subseteq A) \leftrightarrow (A \cap B) \lor_{ℋ} x \subseteq A)$
8	4 1 7	mp3an13	$⊢ x \in C_{ℋ} \to ((A \cap B \subseteq A \land x \subseteq A) \leftrightarrow (A \cap B) \lor_{ℋ} x \subseteq A)$
9		simpr	$⊢ (A \cap B \subseteq A \land x \subseteq A) \to x \subseteq A$
10	8 9	syl6bir	$⊢ x \in C_{ℋ} \to ((A \cap B) \lor_{ℋ} x \subseteq A \to x \subseteq A)$
11	10	adantld	$⊢ x \in C_{ℋ} \to ((A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq A) \to x \subseteq A)$
12		ssin	$⊢ (x \subseteq A \land x \subseteq B) \leftrightarrow x \subseteq A \cap B$
13	12	notbii	$⊢ \neg (x \subseteq A \land x \subseteq B) \leftrightarrow \neg x \subseteq A \cap B$
14		chnle	$⊢ (A \cap B \in C_{ℋ} \land x \in C_{ℋ}) \to (\neg x \subseteq A \cap B \leftrightarrow A \cap B \subset (A \cap B) \lor_{ℋ} x)$
15	4 14	mpan	$⊢ x \in C_{ℋ} \to (\neg x \subseteq A \cap B \leftrightarrow A \cap B \subset (A \cap B) \lor_{ℋ} x)$
16	13 15	syl5bb	$⊢ x \in C_{ℋ} \to (\neg (x \subseteq A \land x \subseteq B) \leftrightarrow A \cap B \subset (A \cap B) \lor_{ℋ} x)$
17	16 8	anbi12d	$⊢ x \in C_{ℋ} \to ((\neg (x \subseteq A \land x \subseteq B) \land (A \cap B \subseteq A \land x \subseteq A)) \leftrightarrow (A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq A))$
18		pm3.21	$⊢ x \subseteq B \to (x \subseteq A \to (x \subseteq A \land x \subseteq B))$
19		orcom	$⊢ ((x \subseteq A \land x \subseteq B) \lor \neg x \subseteq A) \leftrightarrow (\neg x \subseteq A \lor (x \subseteq A \land x \subseteq B))$
20		pm4.55	$⊢ \neg (\neg (x \subseteq A \land x \subseteq B) \land x \subseteq A) \leftrightarrow ((x \subseteq A \land x \subseteq B) \lor \neg x \subseteq A)$
21		imor	$⊢ (x \subseteq A \to (x \subseteq A \land x \subseteq B)) \leftrightarrow (\neg x \subseteq A \lor (x \subseteq A \land x \subseteq B))$
22	19 20 21	3bitr4ri	$⊢ (x \subseteq A \to (x \subseteq A \land x \subseteq B)) \leftrightarrow \neg (\neg (x \subseteq A \land x \subseteq B) \land x \subseteq A)$
23	18 22	sylib	$⊢ x \subseteq B \to \neg (\neg (x \subseteq A \land x \subseteq B) \land x \subseteq A)$
24	23	con2i	$⊢ (\neg (x \subseteq A \land x \subseteq B) \land x \subseteq A) \to \neg x \subseteq B$
25	24	adantrl	$⊢ (\neg (x \subseteq A \land x \subseteq B) \land (A \cap B \subseteq A \land x \subseteq A)) \to \neg x \subseteq B$
26	17 25	syl6bir	$⊢ x \in C_{ℋ} \to ((A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq A) \to \neg x \subseteq B)$
27	11 26	jcad	$⊢ x \in C_{ℋ} \to ((A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq A) \to (x \subseteq A \land \neg x \subseteq B))$
28	6 27	syl	$⊢ x \in HAtoms \to ((A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq A) \to (x \subseteq A \land \neg x \subseteq B))$
29	28	reximia	$⊢ \exists x \in HAtoms (A \cap B \subset (A \cap B) \lor_{ℋ} x \land (A \cap B) \lor_{ℋ} x \subseteq A) \to \exists x \in HAtoms (x \subseteq A \land \neg x \subseteq B)$
30	5 29	syl	$⊢ A \cap B \subset A \to \exists x \in HAtoms (x \subseteq A \land \neg x \subseteq B)$
31	3 30	sylbi	$⊢ \neg A \subseteq B \to \exists x \in HAtoms (x \subseteq A \land \neg x \subseteq B)$
32		sstr2	$⊢ x \subseteq A \to (A \subseteq B \to x \subseteq B)$
33	32	com12	$⊢ A \subseteq B \to (x \subseteq A \to x \subseteq B)$
34	33	ralrimivw	$⊢ A \subseteq B \to \forall x \in HAtoms (x \subseteq A \to x \subseteq B)$
35		iman	$⊢ (x \subseteq A \to x \subseteq B) \leftrightarrow \neg (x \subseteq A \land \neg x \subseteq B)$
36	35	ralbii	$⊢ \forall x \in HAtoms (x \subseteq A \to x \subseteq B) \leftrightarrow \forall x \in HAtoms \neg (x \subseteq A \land \neg x \subseteq B)$
37		ralnex	$⊢ \forall x \in HAtoms \neg (x \subseteq A \land \neg x \subseteq B) \leftrightarrow \neg \exists x \in HAtoms (x \subseteq A \land \neg x \subseteq B)$
38	36 37	bitri	$⊢ \forall x \in HAtoms (x \subseteq A \to x \subseteq B) \leftrightarrow \neg \exists x \in HAtoms (x \subseteq A \land \neg x \subseteq B)$
39	34 38	sylib	$⊢ A \subseteq B \to \neg \exists x \in HAtoms (x \subseteq A \land \neg x \subseteq B)$
40	39	con2i	$⊢ \exists x \in HAtoms (x \subseteq A \land \neg x \subseteq B) \to \neg A \subseteq B$
41	31 40	impbii	$⊢ \neg A \subseteq B \leftrightarrow \exists x \in HAtoms (x \subseteq A \land \neg x \subseteq B)$

Metamath Proof Explorer

Theorem chrelat2i

Proof